| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | term_database_sygus.cpp | 74 TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe) in TermDbSygus() function in CVC4::theory::quantifiers::TermDbSygus
85 bool TermDbSygus::reset( Theory::Effort e ) { in reset()
145 bool TermDbSygus::hasFreeVar( Node n ) { in hasFreeVar()
187 Node TermDbSygus::mkGeneric(const Datatype& dt, in mkGeneric()
234 Node TermDbSygus::canonizeBuiltin(Node n) in canonizeBuiltin()
467 void TermDbSygus::registerEnumerator(Node e, in registerEnumerator()
693 bool TermDbSygus::isEnumerator(Node e) const in isEnumerator()
778 void TermDbSygus::registerSymBreakLemma( in registerSymBreakLemma()
1402 Node TermDbSygus::getAnchor( Node n ) { in getAnchor()
1517 Node TermDbSygus::unfold(Node en) in unfold()
[all …]
|
| H A D | sygus_invariance.h | 29 class TermDbSygus; variable
57 bool is_invariant(TermDbSygus* tds, Node nvn, Node x) in is_invariant()
74 virtual bool invariant(TermDbSygus* tds, Node nvn, Node x) = 0;
114 Node doEvaluateWithUnfolding(TermDbSygus* tds, Node n);
118 bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
184 TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr);
188 bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
220 bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
282 bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
|
| H A D | enum_stream_substitution.h | 36 EnumStreamPermutation(quantifiers::TermDbSygus* tds);
73 quantifiers::TermDbSygus* d_tds;
168 EnumStreamSubstitution(quantifiers::TermDbSygus* tds);
214 quantifiers::TermDbSygus* d_tds;
284 EnumStreamConcrete(quantifiers::TermDbSygus* tds) : d_ess(tds) {} in EnumStreamConcrete()
|
| H A D | sygus_eval_unfold.h | 28 class TermDbSygus; variable
42 SygusEvalUnfold(TermDbSygus* tds);
89 TermDbSygus* d_tds;
|
| H A D | sygus_invariance.cpp | 50 Node EvalSygusInvarianceTest::doEvaluateWithUnfolding(TermDbSygus* tds, Node n) in doEvaluateWithUnfolding()
55 bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) in invariant()
90 TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr) in init()
106 bool EquivSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) in invariant()
174 bool DivByZeroSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) in invariant()
201 bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, in invariant()
|
| H A D | sygus_enumerator.h | 47 SygusEnumerator(TermDbSygus* tds, SynthConjecture* p);
60 TermDbSygus* d_tds;
102 TermDbSygus* tds,
149 TermDbSygus* d_tds;
|
| H A D | sygus_explain.h | 143 SygusExplain(TermDbSygus* tdb) : d_tdb(tdb) {} in SygusExplain()
222 TermDbSygus* d_tdb;
|
| H A D | sygus_grammar_red.cpp | 34 TermDbSygus* tds = qe->getTermDatabaseSygus(); in initialize()
96 void SygusRedundantCons::getGenericList(TermDbSygus* tds, in getGenericList()
|
| H A D | sygus_grammar_red.h | 107 void getGenericList(TermDbSygus* tds,
|
| H A D | term_database_sygus.h | 69 class TermDbSygus {
71 TermDbSygus(context::Context* c, QuantifiersEngine* qe);
72 ~TermDbSygus() {} in ~TermDbSygus()
|
| H A D | sygus_eval_unfold.cpp | 29 SygusEvalUnfold::SygusEvalUnfold(TermDbSygus* tds) : d_tds(tds) {} in SygusEvalUnfold()
65 Node a = TermDbSygus::getAnchor(n[0]); in registerEvalTerm()
|
| H A D | synth_conjecture.cpp | 745 EnumValGeneratorBasic(TermDbSygus* tds, TypeNode tn) : d_tds(tds), d_te(tn) {} in EnumValGeneratorBasic()
784 TermDbSygus* d_tds;
867 TermDbSygus::toStreamSygus("sygus-active-gen", e); in getEnumeratedValue()
869 TermDbSygus::toStreamSygus("sygus-active-gen", absE); in getEnumeratedValue()
927 TermDbSygus::toStreamSygus("sygus-active-gen-debug", absE); in getEnumeratedValue()
946 TermDbSygus::toStreamSygus("sygus-active-gen", absE); in getEnumeratedValue()
948 TermDbSygus::toStreamSygus("sygus-active-gen", v); in getEnumeratedValue()
|
| H A D | sygus_module.h | 142 quantifiers::TermDbSygus* d_tds;
|
| H A D | sygus_repair_const.h | 98 TermDbSygus* d_tds;
|
| H A D | sygus_unif.h | 94 quantifiers::TermDbSygus* d_tds;
|
| H A D | cegis_unif.h | 103 TermDbSygus* d_tds;
|
| H A D | synth_conjecture.h | 166 TermDbSygus* d_tds;
|
| H A D | sygus_grammar_norm.h | 399 TermDbSygus* d_tds;
|
| H A D | sygus_unif_io.cpp | 857 TermDbSygus::toStreamSygus("sygus-pbe", vcc); in constructSolutionNode()
1209 TermDbSygus::toStreamSygus("sygus-sui-dt", csol); in constructSol()
1248 TermDbSygus::toStreamSygus("sygus-sui-dt-debug", val_t); in constructSol()
1533 TermDbSygus::toStreamSygus("sygus-sui-dt", ret_dt); in constructSol()
1549 TermDbSygus::toStreamSygus("sygus-sui-cache", ret_dt); in constructSol()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | candidate_rewrite_filter.h | 114 void initialize(SygusSampler* ss, TermDbSygus* tds, bool useSygusType);
151 TermDbSygus* d_tds;
|
| H A D | sygus_sampler.h | 94 virtual void initializeSygus(TermDbSygus* tds,
177 TermDbSygus* d_tds;
|
| H A D | expr_miner_manager.h | 106 TermDbSygus* d_tds;
|
| H A D | candidate_rewrite_database.h | 91 TermDbSygus* d_tds;
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | quantifiers_engine.h | 48 class TermDbSygus; variable
129 quantifiers::TermDbSygus* getTermDatabaseSygus() const;
352 std::unique_ptr<quantifiers::TermDbSygus> d_sygus_tdb;
|
| /dports/math/cvc4/CVC4-1.7/src/theory/datatypes/ |
| H A D | sygus_simple_sym.h | 90 quantifiers::TermDbSygus* d_tds;
|