/dports/math/yices/yices-2.6.2/tests/unit/ |
H A D | test_bvmux.c | 303 b[0] = true_literal; in test_size1() 306 a[0] = true_literal; in test_size1() 314 c = true_literal; in test_size1() 318 c = true_literal; in test_size1() 322 c = true_literal; in test_size1() 326 c = true_literal; in test_size1() 365 c = true_literal; in test_size1() 369 c = true_literal; in test_size1() 373 c = true_literal; in test_size1() 377 c = true_literal; in test_size1() [all …]
|
H A D | test_gate_manager.c | 319 if (l1 == true_literal) return true_literal; in eval_or() 320 if (l2 == true_literal) return true_literal; in eval_or() 387 check_and_aux(m, true_literal, true_literal); in check_and() 407 check_or_aux(m, true_literal, true_literal); in check_or() 428 check_implies_aux(m, true_literal, true_literal); in check_implies() 448 check_xor_aux(m, true_literal, true_literal); in check_xor() 468 check_iff_aux(m, true_literal, true_literal); in check_iff() 490 check_ite_aux(m, false_literal, true_literal, true_literal); in check_ite() 492 check_ite_aux(m, true_literal, false_literal, true_literal); in check_ite() 493 check_ite_aux(m, true_literal, true_literal, false_literal); in check_ite() [all …]
|
H A D | test_bvdivision.c | 134 a[i] = true_literal; in uint32_to_litarray() 234 return true_literal; in eval_literal() 316 lit[0] = true_literal; in init_random() 579 a[0] = true_literal; in base_test4() 586 b[0] = true_literal; in base_test4() 593 a[1] = true_literal; in base_test4() 600 b[1] = true_literal; in base_test4() 607 a[2] = true_literal; in base_test4() 614 b[2] = true_literal; in base_test4() 621 a[3] = true_literal; in base_test4() [all …]
|
H A D | test_bvcomparators.c | 133 a[i] = true_literal; in uint32_to_litarray() 154 if (a[i] == true_literal) { in print_litarray_as_uint32() 242 lit[0] = true_literal; in init_random() 418 b[0] = true_literal; in test_size1() 420 a[0] = true_literal; in test_size1() 423 a[0] = true_literal; in test_size1() 424 b[0] = true_literal; in test_size1() 431 b[0] = true_literal; in test_size1() 436 a[0] = true_literal; in test_size1() 482 a[i] = true_literal; in base_test4() [all …]
|
H A D | test_bvshift.c | 304 lit[0] = true_literal; in init_random() 601 a[i] = true_literal; in base_test4() 608 b[i] = true_literal; in base_test4() 622 a[0] = true_literal; in base_test4() 629 b[0] = true_literal; in base_test4() 636 a[1] = true_literal; in base_test4() 643 b[1] = true_literal; in base_test4() 650 a[2] = true_literal; in base_test4() 657 b[2] = true_literal; in base_test4() 664 a[3] = true_literal; in base_test4() [all …]
|
H A D | test_bvarith_circuits.c | 133 a[i] = true_literal; in uint32_to_litarray() 299 lit[0] = true_literal; in init_random() 626 a[i] = true_literal; in base_test4() 682 a[0] = true_literal; in base_test4var() 689 b[0] = true_literal; in base_test4var() 696 a[1] = true_literal; in base_test4var() 703 b[1] = true_literal; in base_test4var() 710 a[2] = true_literal; in base_test4var() 717 b[2] = true_literal; in base_test4var() 724 a[3] = true_literal; in base_test4var() [all …]
|
H A D | test_bit_blaster.c.old | 456 for (a = true_literal; a <= false_literal; a++) { 483 for (d = true_literal; d <= false_literal; d++) { 541 f(a, true_literal); 552 f(a, b, true_literal); 566 f(a, b, c, true_literal); 592 a[i] = true_literal; 612 if (a[i] == true_literal) { 639 if (a[i] == true_literal) { 647 if (a[n-1] == true_literal) { 684 f(8, a, true_literal); [all …]
|
/dports/math/py-or-tools/or-tools-9.2/ortools/sat/ |
H A D | sat_base.h | 252 void Enqueue(Literal true_literal, int propagator_id) { in Enqueue() argument 254 trail_[current_info_.trail_index] = true_literal; in Enqueue() 256 info_[true_literal.Variable()] = current_info_; in Enqueue() 257 assignment_.AssignFromTrueLiteral(true_literal); in Enqueue() 262 void EnqueueSearchDecision(Literal true_literal) { in EnqueueSearchDecision() argument 267 void EnqueueWithUnitReason(Literal true_literal) { in EnqueueWithUnitReason() argument 268 Enqueue(true_literal, AssignmentType::kUnitReason); in EnqueueWithUnitReason() 274 void EnqueueWithSameReasonAs(Literal true_literal, in EnqueueWithSameReasonAs() argument 288 if (assignment_.LiteralIsFalse(true_literal)) { in EnqueueWithStoredReason() 290 MutableConflict()->push_back(true_literal); in EnqueueWithStoredReason() [all …]
|
H A D | symmetry.cc | 62 const Literal true_literal = (*trail)[propagation_trail_index_]; in PropagateNext() local 63 if (true_literal.Index() < images_.size()) { in PropagateNext() 64 const std::vector<ImageInfo>& images = images_[true_literal.Index()]; in PropagateNext() 72 if (Enqueue(*trail, true_literal, images[image_index].image, p_trail)) { in PropagateNext() 138 const Literal true_literal = trail[propagation_trail_index_]; in Untrail() local 139 if (true_literal.Index() < images_.size()) { in Untrail() 140 for (ImageInfo& info : images_[true_literal.Index()]) { in Untrail()
|
H A D | clause.cc | 343 drat_proof_handler_->AddClause({true_literal}); in InprocessingFixLiteral() 347 if (!trail_->Assignment().LiteralIsTrue(true_literal)) { in InprocessingFixLiteral() 348 trail_->EnqueueWithUnitReason(true_literal); in InprocessingFixLiteral() 556 drat_proof_handler_->AddClause({true_literal}); in FixLiteral() 559 trail_->EnqueueWithUnitReason(true_literal); in FixLiteral() 694 DCHECK(assignment.LiteralIsTrue(true_literal)); in PropagateOnTrue() 718 reasons_[trail->Index()] = true_literal.Negated(); in PropagateOnTrue() 724 if (true_literal.Index() < at_most_ones_.size()) { in PropagateOnTrue() 732 if (literal == true_literal) { in PropagateOnTrue() 749 reasons_[trail->Index()] = true_literal.Negated(); in PropagateOnTrue() [all …]
|
H A D | sat_solver.h | 97 bool AddUnitClause(Literal true_literal); 248 int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal); 261 int EnqueueDecisionAndBacktrackOnConflict(Literal true_literal); 268 bool EnqueueDecisionIfNotConflicting(Literal true_literal);
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
H A D | smt_literal.cpp | 26 if (*this == true_literal) in display() 39 if (*this == true_literal) in display_smt2() 52 if (*this == true_literal) in display_compact() 63 if (l == true_literal) in operator <<()
|
/dports/math/z3/z3-z3-4.8.13/src/smt/ |
H A D | smt_literal.cpp | 26 if (lit == true_literal) in display() 40 if (lit == true_literal) in display_smt2() 54 if (lit == true_literal) in display_compact() 66 if (l == true_literal) in operator <<()
|
H A D | smt_literal.h | 33 const literal true_literal(true_bool_var, false);
|
/dports/math/yices/yices-2.6.2/src/solvers/bv/ |
H A D | bit_blaster.c | 1478 if (a == true_literal) return true_literal; in bit_blaster_eval_or2() 1480 if (b == true_literal) return true_literal; in bit_blaster_eval_or2() 1507 if (a == true_literal) return true_literal; in bit_blaster_eval_or3() 1508 if (b == true_literal) return true_literal; in bit_blaster_eval_or3() 1509 if (c == true_literal) return true_literal; in bit_blaster_eval_or3() 1538 a = true_literal; in bit_blaster_eval_mux() 1550 b = true_literal; in bit_blaster_eval_mux() 2776 c = true_literal; in bit_blaster_make_bvneg() 2896 c = true_literal; in bit_blaster_make_bvinc() 2951 c = true_literal; in bit_blaster_make_bvdec() [all …]
|
H A D | new_bit_blaster.c | 1479 if (a == true_literal) return true_literal; in bit_blaster_eval_or2() 1481 if (b == true_literal) return true_literal; in bit_blaster_eval_or2() 1497 if (a == true_literal) return true_literal; in bit_blaster_eval_or3() 1498 if (b == true_literal) return true_literal; in bit_blaster_eval_or3() 1499 if (c == true_literal) return true_literal; in bit_blaster_eval_or3() 1529 a = true_literal; in bit_blaster_eval_mux() 1541 b = true_literal; in bit_blaster_eval_mux() 1648 aux = true_literal; in bit_blaster_eval_bveq() 2582 c = true_literal; in bit_blaster_make_bvneg() 3085 c = true_literal; in bvneg_litarray() [all …]
|
/dports/databases/arrow/apache-arrow-6.0.1/c_glib/test/dataset/ |
H A D | test-scanner-builder.rb | 55 true_literal = Arrow::LiteralExpression.new(true_datum) 56 filter = Arrow::CallExpression.new("equal", [visible, true_literal])
|
/dports/math/yices/yices-2.6.2/src/scratch/ |
H A D | bool_vartable.c | 476 table->map[0] = true_literal; in init_bool_vartable() 613 if (l == true_literal) return; // the clause is true in bool_vartable_simplify_and_add_clause() 750 if (l1 == true_literal) return bool_vartable_add_unit_clause(table, l2); in bool_vartable_push_eq() 752 if (l2 == true_literal) return bool_vartable_add_unit_clause(table, l1); in bool_vartable_push_eq() 1272 l = true_literal; in gate_for_truth_table() 1427 if (aux == not(l)) return true_literal; in make_or_aux() 1456 if (l == true_literal) return true_literal; in make_or() 1474 if (l != true_literal) { in make_and() 1500 if (l == true_literal) { in make_xor()
|
/dports/math/stp/stp-2.3.3/include/stp/Sat/ |
H A D | SimplifyingMinisat.h | 65 virtual lbool true_literal() { return ((uint8_t)0); } in true_literal() function
|
H A D | Riss.h | 81 virtual lbool true_literal() { return ((uint8_t)0); } in true_literal() function
|
H A D | MinisatCore.h | 80 virtual lbool true_literal() { return ((uint8_t)0); } in true_literal() function
|
H A D | CryptoMinisat5.h | 76 virtual lbool true_literal() { return ((uint8_t)1); } in true_literal() function
|
H A D | SATSolver.h | 84 virtual lbool true_literal() = 0;
|
/dports/math/z3/z3-z3-4.8.13/src/nlsat/tactic/ |
H A D | goal2nlsat.cpp | 137 case nlsat::atom::EQ: return sign == 0 ? nlsat::true_literal : nlsat::false_literal; in process_atom() 138 case nlsat::atom::LT: return sign < 0 ? nlsat::true_literal : nlsat::false_literal; in process_atom() 139 case nlsat::atom::GT: return sign > 0 ? nlsat::true_literal : nlsat::false_literal; in process_atom() 142 return nlsat::true_literal; in process_atom()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/nlsat/tactic/ |
H A D | goal2nlsat.cpp | 137 case nlsat::atom::EQ: return sign == 0 ? nlsat::true_literal : nlsat::false_literal; in process_atom() 138 case nlsat::atom::LT: return sign < 0 ? nlsat::true_literal : nlsat::false_literal; in process_atom() 139 case nlsat::atom::GT: return sign > 0 ? nlsat::true_literal : nlsat::false_literal; in process_atom() 142 return nlsat::true_literal; in process_atom()
|