Home
last modified time | relevance | path

Searched refs:true_literal (Results 1 – 25 of 127) sorted by relevance

123456

/dports/math/yices/yices-2.6.2/tests/unit/
H A Dtest_bvmux.c303 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 Dtest_gate_manager.c319 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 Dtest_bvdivision.c134 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 Dtest_bvcomparators.c133 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 Dtest_bvshift.c304 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 Dtest_bvarith_circuits.c133 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 Dtest_bit_blaster.c.old456 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 Dsat_base.h252 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 Dsymmetry.cc62 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 Dclause.cc343 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 Dsat_solver.h97 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 Dsmt_literal.cpp26 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 Dsmt_literal.cpp26 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 Dsmt_literal.h33 const literal true_literal(true_bool_var, false);
/dports/math/yices/yices-2.6.2/src/solvers/bv/
H A Dbit_blaster.c1478 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 Dnew_bit_blaster.c1479 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 Dtest-scanner-builder.rb55 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 Dbool_vartable.c476 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 DSimplifyingMinisat.h65 virtual lbool true_literal() { return ((uint8_t)0); } in true_literal() function
H A DRiss.h81 virtual lbool true_literal() { return ((uint8_t)0); } in true_literal() function
H A DMinisatCore.h80 virtual lbool true_literal() { return ((uint8_t)0); } in true_literal() function
H A DCryptoMinisat5.h76 virtual lbool true_literal() { return ((uint8_t)1); } in true_literal() function
H A DSATSolver.h84 virtual lbool true_literal() = 0;
/dports/math/z3/z3-z3-4.8.13/src/nlsat/tactic/
H A Dgoal2nlsat.cpp137 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 Dgoal2nlsat.cpp137 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()

123456