Home
last modified time | relevance | path

Searched refs:refineCounterExample (Results 1 – 11 of 11) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/search/
H A Dsearch.cpp64 bool success = d_core->refineCounterExample(thm); in tryModelGeneration()
102 d_core->refineCounterExample(); in getConcreteModel()
/dports/math/cvc3/cvc3-2.4.1/src/include/
H A Dtheory_core.h406 void refineCounterExample();
407 bool refineCounterExample(Theorem& thm);
H A Dtheory_arith3.h300 void refineCounterExample();
H A Dtheory_arith.h131 virtual void refineCounterExample() = 0;
H A Dtheory.h310 virtual void refineCounterExample() {} in refineCounterExample() function
H A Dtheory_arith_new.h240 void refineCounterExample();
H A Dtheory_arith_old.h327 void refineCounterExample();
/dports/math/cvc3/cvc3-2.4.1/src/theory_core/
H A Dtheory_core.cpp3415 bool TheoryCore::refineCounterExample(Theorem& thm) in refineCounterExample() function in TheoryCore
3420 d_theories[i]->refineCounterExample(); in refineCounterExample()
3429 void TheoryCore::refineCounterExample() in refineCounterExample() function in TheoryCore
3434 d_theories[i]->refineCounterExample(); in refineCounterExample()
/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/
H A Dtheory_arith3.cpp2147 void TheoryArith3::refineCounterExample() in refineCounterExample() function in TheoryArith3
H A Dtheory_arith_new.cpp1298 void TheoryArithNew::refineCounterExample() in refineCounterExample() function in TheoryArithNew
H A Dtheory_arith_old.cpp2726 void TheoryArithOld::refineCounterExample() in refineCounterExample() function in TheoryArithOld