| /dports/devel/hpx/hpx-1.2.1/tests/unit/parallel/algorithms/ |
| H A D | partition_copy_tests.hpp | 192 std::vector<int> c(size), d_true(size), d_false(size); in test_partition_copy_exception() local
199 iterator(std::begin(d_true)), iterator(std::begin(d_false)), in test_partition_copy_exception()
223 std::vector<int> c(size), d_true(size), d_false(size); in test_partition_copy_exception_async() local
231 iterator(std::begin(d_true)), iterator(std::begin(d_false)), in test_partition_copy_exception_async()
262 std::vector<int> c(size), d_true(size), d_false(size); in test_partition_copy_bad_alloc() local
269 iterator(std::begin(d_true)), iterator(std::begin(d_false)), in test_partition_copy_bad_alloc()
292 std::vector<int> c(size), d_true(size), d_false(size); in test_partition_copy_bad_alloc_async() local
300 iterator(std::begin(d_true)), iterator(std::begin(d_false)), in test_partition_copy_bad_alloc_async()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/ |
| H A D | cadical.cpp | 64 d_true = newVar(); in CadicalSolver()
68 d_solver->add(toCadicalVar(d_true)); in CadicalSolver()
102 SatVariable CadicalSolver::trueVar() { return d_true; } in trueVar()
|
| H A D | cryptominisat.cpp | 71 d_true = newVar(); in CryptoMinisatSolver()
75 clause[0] = CMSat::Lit(d_true, false); in CryptoMinisatSolver()
157 return d_true; in trueVar()
|
| H A D | cadical.h | 69 SatVariable d_true; variable
|
| H A D | cryptominisat.h | 46 SatVariable d_true; variable
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/ |
| H A D | full_model_check.cpp | 283 d_true = NodeManager::currentNM()->mkConst(true); in FullModelChecker()
628 if (ev==d_true) { in doExhaustiveInstantiation()
636 if( ev==d_true ){ in doExhaustiveInstantiation()
801 if (ev!=d_true) { in exhaustiveInstantiate()
935 …dc.d_value[i] = dc.d_value[i]==d_true ? d_false : ( dc.d_value[i]==d_false ? d_true : dc.d_value[i… in doNegate()
944 d.addEntry(fm, mkCond(cond), d_true); in doVariableEquality()
961 d.addEntry( fm, mkCond(cond), d_true); in doVariableEquality()
982 d.addEntry(fm, mkCond(cond), d_true); in doVariableRelation()
989 d.addEntry( fm, dc.d_cond[i], d_true); in doVariableRelation()
1213 return vals[0]==vals[1] ? d_true : d_false; in evaluateInterpreted()
[all …]
|
| H A D | model_builder.cpp | 124 if (val != d_qe->getTermUtil()->d_true) in debugModel()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arrays/ |
| H A D | theory_arrays.cpp | 128 d_true = NodeManager::currentNM()->mkConst<bool>(true); in TheoryArrays()
1291 d_equalityEngine.assertEquality(d, true, d_true); in getSkolem()
1534 if (t == d_true) { in mkAnd()
1539 if (*child_it == d_true) { in mkAnd()
1567 return invert ? d_false : d_true; in mkAnd()
2118 if (eq1_r == d_true) { in queueRowLemma()
2125 d_equalityEngine.assertEquality(eq1, true, d_true); in queueRowLemma()
2131 if (eq2_r == d_true) { in queueRowLemma()
2132 d_equalityEngine.assertEquality(eq2, true, d_true); in queueRowLemma()
2225 if (eq1_r == d_true) { in dischargeLemmas()
[all …]
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | inst_propagator.cpp | 30 d_true = NodeManager::currentNM()->mkConst( true ); in EqualityQueryInstProp()
366 if( n==d_true || n==d_false ){ in isPropagateLiteral()
418 ret = pol ? d_true : d_false; in evaluateTermExp()
445 }else if( c==d_true || c==d_false ){ in evaluateTermExp()
458 … ret = evaluateTermExp( n[ c==d_true ? 1 : 2], exp, visited, hasPol, pol, watch_list_out, props ); in evaluateTermExp()
462 ret = c==d_true ? d_false : d_true; in evaluateTermExp()
536 ret = k==kind::AND ? d_true : d_false; in evaluateTermExp()
617 d_conc_to_id[i][d_qy.d_true] = 0; in reset()
754 propagate( lit, pol ? d_qy.d_true : d_qy.d_false, true, ii.d_curr_exp ); in update()
|
| H A D | term_database.cpp | 40 d_true = NodeManager::currentNM()->mkConst(true); in TermDb()
535 }else if( c==d_true || c==d_false ){ in evaluateTerm2()
537 if( ( n.getKind()==kind::AND && c==d_false ) || ( n.getKind()==kind::OR && c==d_true ) ){ in evaluateTerm2()
542 ret = evaluateTerm2( n[ c==d_true ? 1 : 2], visited, qy, useEntailmentTests ); in evaluateTerm2()
580 ret = j==0 ? d_true : d_false; in evaluateTerm2()
722 if( n1==d_true ){ in isEntailed2()
727 return qy->getEngine()->getRepresentative( n1 ) == ( pol ? d_true : d_false ); in isEntailed2()
|
| H A D | equality_infer.h | 44 Node d_true; variable
|
| H A D | extended_rewrite.h | 68 Node d_true; variable
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | sygus_unif_io.cpp | 34 d_true = NodeManager::currentNM()->mkConst(true); in UnifContextIo()
46 Node poln = pol ? d_true : d_false; in updateContext()
51 if (d_vals[i] == d_true) in updateContext()
99 d_vals.push_back(d_true); in initialize()
126 if (d_vals[i] == sui->d_true) in getCurrentStrings()
161 if (d_vals[j] == sui->d_true) in getStringIncrement()
204 if (d_vals[j] == sui->d_true) in isStringSolved()
506 d_true = NodeManager::currentNM()->mkConst(true); in SygusUnifIo()
682 resb = (res.isConst() && res == out) ? d_true : d_false; in notifyEnumeration()
703 Trace("sygus-sui-enum") << (resb == d_true ? "1" : "0"); in notifyEnumeration()
[all …]
|
| H A D | sygus_unif_io.h | 129 Node d_true;
359 Node d_true; variable
|
| H A D | sygus_pbe.h | 197 Node d_true;
|
| /dports/math/cvc4/CVC4-1.7/src/preprocessing/util/ |
| H A D | ite_utilities.h | 176 Node d_true; /* Copy of true. */
216 Node d_true;
335 Node d_true; variable
|
| H A D | ite_utilities.cpp | 298 d_true = NodeManager::currentNM()->mkConst<bool>(true); in ITECompressor()
382 Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2]; in compressBooleanITEs()
660 d_true = NodeManager::currentNM()->mkConst<bool>(true); in ITESimplifier()
962 return ite[0].iteNode(d_true, notIte.eqNode(ite[2])); in attemptLiftEquality()
967 return ite[0].iteNode(notIte.eqNode(ite[1]), d_true); in attemptLiftEquality()
1102 Node res = (cite == constant) ? d_true : d_false; in constantIteEqualsConstant()
1126 d_constantIteEqualsConstantCache[pair] = d_true; in constantIteEqualsConstant()
1128 << instance << "->" << d_true << endl; in constantIteEqualsConstant()
1129 return d_true; in constantIteEqualsConstant()
1648 d_true = NodeManager::currentNM()->mkConst<bool>(true); in ITECareSimplifier()
[all …]
|
| /dports/misc/vxl/vxl-3.3.2/contrib/mul/vil3d/algo/ |
| H A D | vil3d_make_distance_filter.cxx | 89 double d_true = std::sqrt(double(i*i+j*j+k*k)); in vil3d_offset_is_prime() local
100 if (std::fabs(d[a]+d[b]-d_true)<1e-5) return false; in vil3d_offset_is_prime()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/strings/ |
| H A D | regexp_solver.h | 68 Node d_true; variable
|
| H A D | regexp_operation.cpp | 29 d_true(NodeManager::currentNM()->mkConst(true)), in RegExpOpr()
314 Node dnode = d_true; in derivativeS()
334 if(dnode != d_true) { in derivativeS()
783 conc = d_true; in simplifyNRegExp()
823 s1r1 = d_true; in simplifyNRegExp()
838 s2r2 = d_true; in simplifyNRegExp()
857 conc = c_and.size() == 0 ? d_true : in simplifyNRegExp()
875 conc = d_true; in simplifyNRegExp()
1055 conc = d_true; in simplifyPRegExp()
1059 conc = d_true; in simplifyPRegExp()
[all …]
|
| H A D | regexp_operation.h | 45 Node d_true; variable
|
| /dports/math/cvc3/cvc3-2.4.1/src/expr/ |
| H A D | expr_manager.cpp | 118 d_true = newLeafExpr(TRUE_EXPR); in ExprManager()
119 d_true.setType(Type::typeBool(this)); in ExprManager()
155 d_true = Expr(); in clear()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arith/ |
| H A D | congruence_manager.cpp | 56 d_true = NodeManager::currentNM()->mkConst( true ); in ArithCongruenceManager()
492 Assert( eq_exp==d_true ); in fixpointInfer()
496 req_exp = d_true; in fixpointInfer()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | ext_theory.h | 201 Node d_true; variable
|
| H A D | theory_model.h | 306 Node d_true; variable
|