This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(declare-fun t1 () Int) | |
(declare-fun t2 () Int) | |
(declare-fun t3 () Int) | |
(declare-fun t4 () Int) | |
(declare-fun t5 () Int) | |
(declare-fun t6 () Int) | |
(assert | |
(and | |
(> (+ (- (+ t3 (* 1.000000 t4)) (* 4 t5)) (* 16.000000 t6)) 0) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include "dreal/dreal.h" | |
int main() { | |
dreal::Variable tmp_var0("t1", dreal::Variable::Type::INTEGER); | |
dreal::Variable tmp_var1("t2", dreal::Variable::Type::INTEGER); | |
dreal::Variable tmp_var2("t3", dreal::Variable::Type::INTEGER); | |
dreal::Variable tmp_var3("t4", dreal::Variable::Type::INTEGER); | |
dreal::Variable tmp_var4("t5", dreal::Variable::Type::INTEGER); | |
dreal::Variable tmp_var5("t5", dreal::Variable::Type::INTEGER); |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include <t1p.h> | |
#include <ap_abstract0.h> | |
#include <stdio.h> | |
/* This is an example to demonstrate a bug in Apron's taylor1plus domain. We | |
* maintain two abstract values, v1 and v2. In a loop we do the following: | |
* - Append v2 to v1 to generate a new abstract value with dimension equal to | |
* the sum of the dimensions of v1 and v2. | |
* - Perform a linear assignment on this abstract value. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include <t1p.h> | |
#include <ap_abstract0.h> | |
int main(int argc, char** argv) { | |
ap_manager_t* man = t1p_manager_alloc(); | |
int in_size = 10; | |
int out_size = 5; | |
ap_interval_t** itv = ap_interval_array_alloc(in_size); |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include <iostream> | |
#include <opt_oct.h> | |
int main() { | |
elina_manager_t* man = opt_oct_manager_alloc(); | |
elina_interval_t** itv1 = (elina_interval_t**) malloc(2 * | |
sizeof(elina_interval_t*)); | |
itv1[0] = elina_interval_alloc(); |