Searched refs:var_bound (Results 1 – 9 of 9) sorted by relevance
/dports/math/cvc4/CVC4-1.7/src/theory/ |
H A D | sort_inference.cpp | 125 std::map<Node, Node> var_bound; in initialize() local 126 process(a, var_bound, visited); in initialize() 170 std::map<Node, Node> var_bound; in initialize() local 201 std::map<Node, Node> var_bound; in simplify() local 298 std::map<Node, Node> var_bound; in computeMonotonicity() local 385 var_bound[ n[0][i] ] = n; in process() 467 if( it!=var_bound.end() ){ in process() 515 var_bound[n[0][i]] = n; in processMonotonic() 528 if( var_bound.find( n[i] )!=var_bound.end() ){ in processMonotonic() 634 var_bound[ n[0][i] ] = v; in simplifyNode() [all …]
|
H A D | sort_inference.h | 81 int process( Node n, std::map< Node, Node >& var_bound, std::map< Node, int >& visited ); 84 …void processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound, std::map<… 98 std::map<Node, Node>& var_bound,
|
/dports/math/z3/z3-z3-4.8.13/src/tactic/arith/ |
H A D | bound_propagator.h | 166 typedef std::pair<var, bound *> var_bound; typedef 167 svector<var_bound> m_todo;
|
H A D | bound_propagator.cpp | 800 svector<var_bound> & todo = const_cast<bound_propagator*>(this)->m_todo; in explain() 803 todo.push_back(var_bound(x, b)); in explain() 806 var_bound & vb = todo[qhead]; in explain() 833 todo.push_back(var_bound(x_i, b)); in explain()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/arith/ |
H A D | bound_propagator.h | 166 typedef std::pair<var, bound *> var_bound; typedef 167 svector<var_bound> m_todo;
|
H A D | bound_propagator.cpp | 800 svector<var_bound> & todo = const_cast<bound_propagator*>(this)->m_todo; in explain() 803 todo.push_back(var_bound(x, b)); in explain() 806 var_bound & vb = todo[qhead]; in explain() 833 todo.push_back(var_bound(x_i, b)); in explain()
|
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/ |
H A D | inst_match_generator.cpp | 631 std::map< Node, bool > var_bound; in InstMatchGeneratorMultiLinear() local 645 if( var_bound.find( v )!=var_bound.end() ){ in InstMatchGeneratorMultiLinear() 665 var_bound[var_contains[mp][i]] = true; in InstMatchGeneratorMultiLinear()
|
/dports/math/z3/z3-z3-4.8.13/src/test/lp/ |
H A D | nla_solver_test.cpp | 23 svector<lpvar> get_monic(int monic_size, int var_bound, random_gen& rand) { in get_monic() argument 26 lpvar j = rand() % var_bound; in get_monic()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/test/lp/ |
H A D | nla_solver_test.cpp | 23 svector<lpvar> get_monic(int monic_size, int var_bound, random_gen& rand) { 26 lpvar j = rand() % var_bound;
|