diff options
Diffstat (limited to 'src/theory/quantifiers')
163 files changed, 721 insertions, 538 deletions
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 577b2c31f..bb0cdde83 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -2,9 +2,9 @@ /*! \file alpha_equivalence.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 4ab45b015..5ab7d0fc2 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index 08e215d72..5d1967bb4 100644 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -2,9 +2,9 @@ /*! \file anti_skolem.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h index 162140ff1..e02c85866 100644 --- a/src/theory/quantifiers/anti_skolem.h +++ b/src/theory/quantifiers/anti_skolem.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 2525f5d18..24e3a85b5 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -2,9 +2,9 @@ /*! \file bv_inverter.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner, Andrew Reynolds + ** Aina Niemetz, Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index ad16a2ed9..b4cfe2bed 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Mathias Preiner, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/bv_inverter_utils.cpp b/src/theory/quantifiers/bv_inverter_utils.cpp index 8ad26a422..e01af3f38 100644 --- a/src/theory/quantifiers/bv_inverter_utils.cpp +++ b/src/theory/quantifiers/bv_inverter_utils.cpp @@ -1,10 +1,10 @@ /********************* */ -/*! \file bv_inverter.cpp +/*! \file bv_inverter_utils.cpp ** \verbatim ** Top contributors (to current version): ** Aina Niemetz, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/bv_inverter_utils.h b/src/theory/quantifiers/bv_inverter_utils.h index 0fec00579..4ab677f0e 100644 --- a/src/theory/quantifiers/bv_inverter_utils.h +++ b/src/theory/quantifiers/bv_inverter_utils.h @@ -1,10 +1,10 @@ /********************* */ -/*! \file bv_inverter.cpp +/*! \file bv_inverter_utils.h ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner + ** Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 2d2e9ce30..e00bc957f 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -2,9 +2,9 @@ /*! \file candidate_rewrite_database.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -69,9 +69,29 @@ void CandidateRewriteDatabase::initializeSygus(const std::vector<Node>& vars, } bool CandidateRewriteDatabase::addTerm(Node sol, + bool rec, std::ostream& out, bool& rew_print) { + // have we added this term before? + std::unordered_map<Node, bool, NodeHashFunction>::iterator itac = + d_add_term_cache.find(sol); + if (itac != d_add_term_cache.end()) + { + return itac->second; + } + + if (rec) + { + // if recursive, we first add all subterms + for (const Node& solc : sol) + { + // whether a candidate rewrite is printed for any subterm is irrelevant + bool rew_printc = false; + addTerm(solc, rec, out, rew_printc); + } + } + // register the term bool is_unique_term = true; Node eq_sol = d_sampler->registerTerm(sol); // eq_sol is a candidate solution that is equivalent to sol @@ -117,9 +137,9 @@ bool CandidateRewriteDatabase::addTerm(Node sol, // options as the SmtEngine we belong to, where we ensure that // produce-models is set. bool needExport = false; - ExprManagerMapCollection varMap; ExprManager em(nm->getOptions()); std::unique_ptr<SmtEngine> rrChecker; + ExprManagerMapCollection varMap; initializeChecker(rrChecker, em, varMap, crr, needExport); Result r = rrChecker->checkSat(); Trace("rr-check") << "...result : " << r << std::endl; @@ -252,13 +272,18 @@ bool CandidateRewriteDatabase::addTerm(Node sol, // it discards it as a redundant candidate rewrite rule before // checking its correctness. } + d_add_term_cache[sol] = is_unique_term; return is_unique_term; } -bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) +bool CandidateRewriteDatabase::addTerm(Node sol, bool rec, std::ostream& out) { bool rew_print = false; - return addTerm(sol, out, rew_print); + return addTerm(sol, rec, out, rew_print); +} +bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) +{ + return addTerm(sol, false, out); } void CandidateRewriteDatabase::setSilent(bool flag) { d_silent = flag; } @@ -298,7 +323,7 @@ bool CandidateRewriteDatabaseGen::addTerm(Node n, std::ostream& out) Trace("synth-rr-dbg") << "...finish." << std::endl; } Trace("synth-rr-dbg") << "Add term " << nr << " for " << tn << std::endl; - return itc->second.addTerm(nr, out); + return itc->second.addTerm(nr, false, out); } } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 5b8ffbd94..9daaa970e 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -71,9 +71,13 @@ class CandidateRewriteDatabase : public ExprMiner * cause a candidate-rewrite to be printed on the output stream out. * We return true if the term sol is distinct (up to equivalence) with * all previous terms added to this class. The argument rew_print is set to - * true if this class printed a rewrite. + * true if this class printed a rewrite involving sol. + * + * If the flag rec is true, then we also recursively add all subterms of sol + * to this class as well. */ - bool addTerm(Node sol, std::ostream& out, bool& rew_print); + bool addTerm(Node sol, bool rec, std::ostream& out, bool& rew_print); + bool addTerm(Node sol, bool rec, std::ostream& out); bool addTerm(Node sol, std::ostream& out) override; /** sets whether this class should output candidate rewrites it finds */ void setSilent(bool flag); @@ -93,6 +97,8 @@ class CandidateRewriteDatabase : public ExprMiner bool d_using_sygus; /** candidate rewrite filter */ CandidateRewriteFilter d_crewrite_filter; + /** the cache for results of addTerm */ + std::unordered_map<Node, bool, NodeHashFunction> d_add_term_cache; /** if true, we silence the output of candidate rewrites */ bool d_silent; }; @@ -115,7 +121,8 @@ class CandidateRewriteDatabaseGen * This registers term n with this class. We generate the candidate rewrite * database of the appropriate type (if not allocated already), and register * n with this database. This may result in "candidate-rewrite" being - * printed on the output stream out. + * printed on the output stream out. We return true if the term sol is + * distinct (up to equivalence) with all previous terms added to this class. */ bool addTerm(Node n, std::ostream& out); diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp index 0d3878149..53c40464f 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.cpp +++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -290,6 +290,12 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n) // ----- check rewriting redundancy if (keep && options::sygusRewSynthFilterCong()) { + // When using sygus types, this filtering applies to the builtin versions + // of n and eq_n. This means that we may filter out a rewrite rule for one + // sygus type based on another, e.g. we won't report x=x+0 for both A and B + // in: + // A -> x | 0 | A+A + // B -> x | 0 | B+B Trace("cr-filter-debug") << "Check equal rewrite pair..." << std::endl; if (d_drewrite->areEqual(bn, beq_n)) { @@ -309,7 +315,9 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n) Node bni = d_drewrite->toInternal(bn); if (!bni.isNull()) { - if (!d_match_trie.getMatches(bni, &d_ssenm)) + // as with congruence filtering, we cache based on the builtin type + TypeNode tn = bn.getType(); + if (!d_match_trie[tn].getMatches(bni, &d_ssenm)) { keep = false; Trace("cr-filter") << "...redundant (matchable)" << std::endl; @@ -357,6 +365,8 @@ void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n) } if (options::sygusRewSynthFilterMatch()) { + // cache based on the builtin type + TypeNode tn = bn.getType(); // add to match information for (unsigned r = 0; r < 2; r++) { @@ -369,7 +379,7 @@ void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n) Node ti = d_drewrite->toInternal(t); if (!ti.isNull()) { - d_match_trie.addTerm(ti); + d_match_trie[tn].addTerm(ti); } } d_pairs[t].insert(to); diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h index ca071faa4..63d5d6fec 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.h +++ b/src/theory/quantifiers/candidate_rewrite_filter.h @@ -2,9 +2,9 @@ /*! \file candidate_rewrite_filter.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -165,14 +165,16 @@ class CandidateRewriteFilter * detail, if (t,s) is a relevant pair, then t in d_pairs[s]. */ std::map<Node, std::unordered_set<Node, NodeHashFunction> > d_pairs; - /** Match trie storing all terms in the domain of d_pairs. + /** + * For each (builtin) type, a match trie storing all terms in the domain of + * d_pairs. * * Notice that we store d_drewrite->toInternal(t) instead of t, for each * term t, so that polymorphism is handled properly. In particular, this * prevents matches between terms select( x, y ) and select( z, y ) where * the type of x and z are different. */ - MatchTrie d_match_trie; + std::map<TypeNode, MatchTrie> d_match_trie; /** Notify class */ class CandidateRewriteFilterNotifyMatch : public NotifyMatch { diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 4ea006d54..fa02c6d09 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -2,9 +2,9 @@ /*! \file ceg_arith_instantiator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h index b6e22329d..5bc75f801 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h @@ -2,9 +2,9 @@ /*! \file ceg_arith_instantiator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 272914c25..28a24d884 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Mathias Preiner, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h index 35bc6c042..b9c35b3e0 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h @@ -2,9 +2,9 @@ /*! \file ceg_bv_instantiator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Aina Niemetz + ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp index b74d358ac..b351dc83c 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp @@ -1,10 +1,10 @@ /********************* */ -/*! \file ceg_bv_instantiator.cpp +/*! \file ceg_bv_instantiator_utils.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Aina Niemetz + ** Mathias Preiner, Aina Niemetz, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h index 551ce08e0..3156e745c 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h @@ -1,10 +1,10 @@ /********************* */ -/*! \file ceg_bv_instantiator.cpp +/*! \file ceg_bv_instantiator_utils.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Aina Niemetz + ** Mathias Preiner, Aina Niemetz, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp index e56d5f5db..0bdcbe0d7 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp @@ -2,9 +2,9 @@ /*! \file ceg_dt_instantiator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h index 6cf3bdf42..ea3db0e9b 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h @@ -2,9 +2,9 @@ /*! \file ceg_dt_instantiator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp index df6690273..f0ea7ab7b 100644 --- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp @@ -2,9 +2,9 @@ /*! \file ceg_epr_instantiator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h index f5057ad86..2ed76ba27 100644 --- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h @@ -2,9 +2,9 @@ /*! \file ceg_epr_instantiator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 46649154e..b11358543 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -2,9 +2,9 @@ /*! \file ceg_instantiator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index ae191cf91..a813c91b0 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -2,9 +2,9 @@ /*! \file ceg_instantiator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner + ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 3ea3e72e4..7cfda5ba1 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -2,9 +2,9 @@ /*! \file inst_strategy_cegqi.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters + ** Andrew Reynolds, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index 0a19727b8..c5c90b64a 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -2,9 +2,9 @@ /*! \file inst_strategy_cegqi.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner + ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 7408678e7..1d9ed1639 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -2,9 +2,9 @@ /*! \file conjecture_generator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Dejan Jovanovic + ** Andrew Reynolds, Aina Niemetz, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 8fff7eafe..236c08138 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp index f48f73aee..cd73ffe33 100644 --- a/src/theory/quantifiers/dynamic_rewrite.cpp +++ b/src/theory/quantifiers/dynamic_rewrite.cpp @@ -2,9 +2,9 @@ /*! \file dynamic_rewrite.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h index 50bae0268..6d0a1625c 100644 --- a/src/theory/quantifiers/dynamic_rewrite.h +++ b/src/theory/quantifiers/dynamic_rewrite.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 612a1938a..cb0fcaf50 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -2,9 +2,9 @@ /*! \file candidate_generator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters + ** Andrew Reynolds, Morgan Deters, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h index da4ec2d83..d2718fa1f 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.h +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 2fcfa19d9..7598e6fdc 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -270,6 +270,11 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) // Assert( f==value ); for (unsigned k = 0, size = args.size(); k < size; k++) { + // must now subsitute back, to handle cases like + // (@ x y) matching (@ t (@ t s)) + // where the above substitution would produce (@ x (@ x s)), + // but the argument should be (@ t s). + args[k] = args[k].substitute(var, value); Node val = args[k]; std::map<unsigned, Node>::iterator itf = fixed_vals.find(k); if (itf == fixed_vals.end()) diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index 8840c949f..b57db5799 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index f26df5b79..0a4386db9 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -2,9 +2,9 @@ /*! \file inst_match_generator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 83d4ce82e..f9fd2be25 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -2,9 +2,9 @@ /*! \file inst_match_generator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Clark Barrett + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 6784fb8e3..8f671fb55 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -2,9 +2,9 @@ /*! \file inst_strategy_e_matching.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters + ** Andrew Reynolds, Morgan Deters, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index a8d53cf4b..d715d7f7a 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 2aa8af53d..d2650f01f 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index c94320b74..cd82e67a3 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -2,9 +2,9 @@ /*! \file instantiation_engine.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index b50deea11..31bd1aa96 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index bbd7c386b..9a65f0c02 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp index f4a4a34a7..ef80af5f5 100644 --- a/src/theory/quantifiers/equality_infer.cpp +++ b/src/theory/quantifiers/equality_infer.cpp @@ -2,9 +2,9 @@ /*! \file equality_infer.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters, Tianyi Liang ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h index 49d208d99..be1d6d81d 100644 --- a/src/theory/quantifiers/equality_infer.h +++ b/src/theory/quantifiers/equality_infer.h @@ -2,9 +2,9 @@ /*! \file equality_infer.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli + ** Andrew Reynolds, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index ae560c5e5..030b0dccb 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -2,9 +2,9 @@ /*! \file equality_query.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index 8f836f9c6..9b62c5714 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -2,9 +2,9 @@ /*! \file equality_query.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index b65d1c522..98d07fdea 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -2,9 +2,9 @@ /*! \file expr_miner.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -87,9 +87,11 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, try { checker.reset(new SmtEngine(&em)); + checker->setIsInternalSubsolver(); checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true); checker->setLogic(smt::currentSmtEngine()->getLogicInfo()); checker->setOption("sygus-rr-synth-input", false); + checker->setOption("sygus-abduct", false); checker->setOption("input-language", "smt2"); Expr equery = squery.toExpr().exportTo(&em, varMap); checker->assertFormula(equery); @@ -129,9 +131,9 @@ Result ExprMiner::doCheck(Node query) } NodeManager* nm = NodeManager::currentNM(); bool needExport = false; - ExprManagerMapCollection varMap; ExprManager em(nm->getOptions()); std::unique_ptr<SmtEngine> smte; + ExprManagerMapCollection varMap; initializeChecker(smte, em, varMap, queryr, needExport); return smte->checkSat(); } diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index 59d9989c5..9420b495a 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp index a808d386c..3db0e14ab 100644 --- a/src/theory/quantifiers/expr_miner_manager.cpp +++ b/src/theory/quantifiers/expr_miner_manager.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -15,6 +15,8 @@ #include "theory/quantifiers/expr_miner_manager.h" #include "theory/quantifiers_engine.h" +#include "options/quantifiers_options.h" + namespace CVC4 { namespace theory { namespace quantifiers { @@ -140,7 +142,7 @@ bool ExpressionMinerManager::addTerm(Node sol, bool ret = true; if (d_doRewSynth) { - ret = d_crd.addTerm(sol, out, rew_print); + ret = d_crd.addTerm(sol, options::sygusRewSynthRec(), out, rew_print); } // a unique term, let's try the query generator diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h index d817d3775..dc0a8fab5 100644 --- a/src/theory/quantifiers/expr_miner_manager.h +++ b/src/theory/quantifiers/expr_miner_manager.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 46dcb7151..0fbd971fd 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -2,9 +2,9 @@ /*! \file extended_rewrite.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index da77bda51..920732e0f 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 5eb65ed21..5428d9f1a 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -2,9 +2,9 @@ /*! \file first_order_model.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index b96b42dc2..dc257ea0a 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -2,9 +2,9 @@ /*! \file first_order_model.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Paul Meng + ** Andrew Reynolds, Paul Meng, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index cafa4a749..e15fc85bb 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -2,9 +2,9 @@ /*! \file bounded_integers.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Andres Noetzli, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index b3132a4a7..1eab28fd9 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 481048105..ace5c2b26 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -2,9 +2,9 @@ /*! \file full_model_check.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Kshitij Bansal + ** Andrew Reynolds, Morgan Deters, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index f0f9a1798..d662898c3 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index 8ef30fc4d..51cd8481f 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -2,9 +2,9 @@ /*! \file model_builder.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index b73716169..b5f9c809a 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -2,9 +2,9 @@ /*! \file model_builder.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner + ** Andrew Reynolds, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index d2579b4ee..5609cade6 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -266,7 +266,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ } d_triedLemmas += mb->getNumTriedLemmas()-prev_tlem; d_addedLemmas += mb->getNumAddedLemmas()-prev_alem; - d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += mb->getNumAddedLemmas(); + d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += + (mb->getNumAddedLemmas() - prev_alem); }else{ if( Trace.isOn("fmf-exh-inst-debug") ){ Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index a11115f33..4202988ae 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -2,9 +2,9 @@ /*! \file model_engine.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 1671fa1a0..185a349c0 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -2,9 +2,9 @@ /*! \file fun_def_process.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h index 78adc710c..f455d4a47 100644 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index a16e03420..069d5b888 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -2,9 +2,9 @@ /*! \file inst_match.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Clark Barrett + ** Andrew Reynolds, Morgan Deters, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 5695d1294..db2f7b8a0 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index aba4a3b5e..8b8689835 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -2,9 +2,9 @@ /*! \file inst_match_trie.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index 50df50786..6f5b16bb1 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -2,9 +2,9 @@ /*! \file inst_match_trie.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index 15dd35c26..56be1506c 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -2,9 +2,9 @@ /*! \file inst_propagator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index 1ba359228..d82991b0a 100644 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h @@ -2,9 +2,9 @@ /*! \file inst_propagator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 9d70d0d4b..7a2f62864 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -2,9 +2,9 @@ /*! \file inst_strategy_enumerative.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -70,46 +70,89 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) doCheck = quant_e == QEFFORT_LAST_CALL; fullEffort = !d_quantEngine->hasAddedLemma(); } - if (doCheck) + if (!doCheck) { - double clSet = 0; - if (Trace.isOn("fs-engine")) - { - clSet = double(clock()) / double(CLOCKS_PER_SEC); - Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" - << std::endl; - } - int addedLemmas = 0; - for (unsigned i = 0; - i < d_quantEngine->getModel()->getNumAssertedQuantifiers(); - i++) + return; + } + double clSet = 0; + if (Trace.isOn("fs-engine")) + { + clSet = double(clock()) / double(CLOCKS_PER_SEC); + Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" + << std::endl; + } + unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; + unsigned rend = fullEffort ? 1 : rstart; + unsigned addedLemmas = 0; + // First try in relevant domain of all quantified formulas, if no + // instantiations exist, try arbitrary ground terms. + // Notice that this stratification of effort levels makes it so that some + // quantified formulas may not be instantiated (if they have no instances + // at effort level r=0 but another quantified formula does). We prefer + // this stratification since effort level r=1 may be highly expensive in the + // case where we have a quantified formula with many entailed instances. + FirstOrderModel* fm = d_quantEngine->getModel(); + RelevantDomain* rd = d_quantEngine->getRelevantDomain(); + unsigned nquant = fm->getNumAssertedQuantifiers(); + std::map<Node, bool> alreadyProc; + for (unsigned r = rstart; r <= rend; r++) + { + if (rd || r > 0) { - Node q = d_quantEngine->getModel()->getAssertedQuantifier(i, true); - if (d_quantEngine->hasOwnership(q, this) - && d_quantEngine->getModel()->isQuantifierActive(q)) + if (r == 0) + { + Trace("inst-alg") << "-> Relevant domain instantiate..." << std::endl; + Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl; + rd->compute(); + Trace("inst-alg-debug") << "...finished" << std::endl; + } + else + { + Trace("inst-alg") << "-> Ground term instantiate..." << std::endl; + } + for (unsigned i = 0; i < nquant; i++) { - if (process(q, fullEffort)) + Node q = fm->getAssertedQuantifier(i, true); + bool doProcess = d_quantEngine->hasOwnership(q, this) + && fm->isQuantifierActive(q) + && alreadyProc.find(q) == alreadyProc.end(); + if (doProcess) { - // added lemma - addedLemmas++; - if (d_quantEngine->inConflict()) + if (process(q, fullEffort, r == 0)) { - break; + // don't need to mark this if we are not stratifying + if (!options::fullSaturateStratify()) + { + alreadyProc[q] = true; + } + // added lemma + addedLemmas++; + if (d_quantEngine->inConflict()) + { + break; + } } } } + if (d_quantEngine->inConflict() + || (addedLemmas > 0 && options::fullSaturateStratify())) + { + // we break if we are in conflict, or if we added any lemma at this + // effort level and we stratify effort levels. + break; + } } - if (Trace.isOn("fs-engine")) - { - Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl; - double clSet2 = double(clock()) / double(CLOCKS_PER_SEC); - Trace("fs-engine") << "Finished full saturation engine, time = " - << (clSet2 - clSet) << std::endl; - } + } + if (Trace.isOn("fs-engine")) + { + Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl; + double clSet2 = double(clock()) / double(CLOCKS_PER_SEC); + Trace("fs-engine") << "Finished full saturation engine, time = " + << (clSet2 - clSet) << std::endl; } } -bool InstStrategyEnum::process(Node f, bool fullEffort) +bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) { // ignore if constant true (rare case of non-standard quantifier whose body is // rewritten to true) @@ -117,178 +160,156 @@ bool InstStrategyEnum::process(Node f, bool fullEffort) { return false; } - // first, try from relevant domain RelevantDomain* rd = d_quantEngine->getRelevantDomain(); - unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; - unsigned rend = fullEffort ? 1 : rstart; - for (unsigned r = rstart; r <= rend; r++) + unsigned final_max_i = 0; + std::vector<unsigned> maxs; + std::vector<bool> max_zero; + bool has_zero = false; + std::map<TypeNode, std::vector<Node> > term_db_list; + std::vector<TypeNode> ftypes; + TermDb* tdb = d_quantEngine->getTermDatabase(); + EqualityQuery* qy = d_quantEngine->getEqualityQuery(); + // iterate over substitutions for variables + for (unsigned i = 0; i < f[0].getNumChildren(); i++) { - if (rd || r > 0) + TypeNode tn = f[0][i].getType(); + ftypes.push_back(tn); + unsigned ts; + if (isRd) { - if (r == 0) + ts = rd->getRDomain(f, i)->d_terms.size(); + } + else + { + ts = tdb->getNumTypeGroundTerms(tn); + std::map<TypeNode, std::vector<Node> >::iterator ittd = + term_db_list.find(tn); + if (ittd == term_db_list.end()) { - Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." - << std::endl; - Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl; - rd->compute(); - Trace("inst-alg-debug") << "...finished" << std::endl; + std::map<Node, Node> reps_found; + for (unsigned j = 0; j < ts; j++) + { + Node gt = tdb->getTypeGroundTerm(ftypes[i], j); + if (!options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(gt)) + { + Node rep = qy->getRepresentative(gt); + if (reps_found.find(rep) == reps_found.end()) + { + reps_found[rep] = gt; + term_db_list[tn].push_back(gt); + } + } + } + ts = term_db_list[tn].size(); } else { - Trace("inst-alg") << "-> Ground term instantiate " << f << "..." - << std::endl; + ts = ittd->second.size(); } - unsigned final_max_i = 0; - std::vector<unsigned> maxs; - std::vector<bool> max_zero; - bool has_zero = false; - std::map<TypeNode, std::vector<Node> > term_db_list; - std::vector<TypeNode> ftypes; - // iterate over substitutions for variables - for (unsigned i = 0; i < f[0].getNumChildren(); i++) + } + // consider a default value if at full effort + max_zero.push_back(fullEffort && ts == 0); + ts = (fullEffort && ts == 0) ? 1 : ts; + Trace("inst-alg-rd") << "Variable " << i << " has " << ts + << " in relevant domain." << std::endl; + if (ts == 0) + { + has_zero = true; + break; + } + maxs.push_back(ts); + if (ts > final_max_i) + { + final_max_i = ts; + } + } + if (!has_zero) + { + Trace("inst-alg-rd") << "Will do " << final_max_i + << " stages of instantiation." << std::endl; + unsigned max_i = 0; + bool success; + Instantiate* ie = d_quantEngine->getInstantiate(); + while (max_i <= final_max_i) + { + Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl; + std::vector<unsigned> childIndex; + int index = 0; + do { - TypeNode tn = f[0][i].getType(); - ftypes.push_back(tn); - unsigned ts; - if (r == 0) - { - ts = rd->getRDomain(f, i)->d_terms.size(); - } - else + while (index >= 0 && index < (int)f[0].getNumChildren()) { - ts = d_quantEngine->getTermDatabase()->getNumTypeGroundTerms(tn); - std::map<TypeNode, std::vector<Node> >::iterator ittd = - term_db_list.find(tn); - if (ittd == term_db_list.end()) + if (index == static_cast<int>(childIndex.size())) { - std::map<Node, Node> reps_found; - for (unsigned j = 0; j < ts; j++) - { - Node gt = d_quantEngine->getTermDatabase()->getTypeGroundTerm( - ftypes[i], j); - if (!options::cbqi() - || !quantifiers::TermUtil::hasInstConstAttr(gt)) - { - Node rep = - d_quantEngine->getEqualityQuery()->getRepresentative(gt); - if (reps_found.find(rep) == reps_found.end()) - { - reps_found[rep] = gt; - term_db_list[tn].push_back(gt); - } - } - } - ts = term_db_list[tn].size(); + childIndex.push_back(-1); } else { - ts = ittd->second.size(); + Assert(index == static_cast<int>(childIndex.size()) - 1); + unsigned nv = childIndex[index] + 1; + if (nv < maxs[index] && nv <= max_i) + { + childIndex[index] = nv; + index++; + } + else + { + childIndex.pop_back(); + index--; + } } } - // consider a default value if at full effort - max_zero.push_back(fullEffort && ts == 0); - ts = (fullEffort && ts == 0) ? 1 : ts; - Trace("inst-alg-rd") << "Variable " << i << " has " << ts - << " in relevant domain." << std::endl; - if (ts == 0) + success = index >= 0; + if (success) { - has_zero = true; - break; - } - else - { - maxs.push_back(ts); - if (ts > final_max_i) + if (Trace.isOn("inst-alg-rd")) { - final_max_i = ts; + Trace("inst-alg-rd") << "Try instantiation { "; + for (unsigned i : childIndex) + { + Trace("inst-alg-rd") << i << " "; + } + Trace("inst-alg-rd") << "}" << std::endl; } - } - } - if (!has_zero) - { - Trace("inst-alg-rd") << "Will do " << final_max_i - << " stages of instantiation." << std::endl; - unsigned max_i = 0; - bool success; - while (max_i <= final_max_i) - { - Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl; - std::vector<unsigned> childIndex; - int index = 0; - do + // try instantiation + std::vector<Node> terms; + for (unsigned i = 0, nchild = f[0].getNumChildren(); i < nchild; i++) { - while (index >= 0 && index < (int)f[0].getNumChildren()) + if (max_zero[i]) { - if (index == (int)childIndex.size()) - { - childIndex.push_back(-1); - } - else - { - Assert(index == (int)(childIndex.size()) - 1); - unsigned nv = childIndex[index] + 1; - if (nv < maxs[index] && nv <= max_i) - { - childIndex[index] = nv; - index++; - } - else - { - childIndex.pop_back(); - index--; - } - } + // no terms available, will report incomplete instantiation + terms.push_back(Node::null()); + Trace("inst-alg-rd") << " null" << std::endl; } - success = index >= 0; - if (success) + else if (isRd) { - Trace("inst-alg-rd") << "Try instantiation { "; - for (unsigned j = 0; j < childIndex.size(); j++) - { - Trace("inst-alg-rd") << childIndex[j] << " "; - } - Trace("inst-alg-rd") << "}" << std::endl; - // try instantiation - std::vector<Node> terms; - for (unsigned i = 0; i < f[0].getNumChildren(); i++) - { - if (max_zero[i]) - { - // no terms available, will report incomplete instantiation - terms.push_back(Node::null()); - Trace("inst-alg-rd") << " null" << std::endl; - } - else if (r == 0) - { - terms.push_back(rd->getRDomain(f, i)->d_terms[childIndex[i]]); - Trace("inst-alg-rd") - << " " << rd->getRDomain(f, i)->d_terms[childIndex[i]] - << std::endl; - } - else - { - Assert(childIndex[i] < term_db_list[ftypes[i]].size()); - terms.push_back(term_db_list[ftypes[i]][childIndex[i]]); - Trace("inst-alg-rd") << " " - << term_db_list[ftypes[i]][childIndex[i]] - << std::endl; - } - } - if (d_quantEngine->getInstantiate()->addInstantiation(f, terms)) - { - Trace("inst-alg-rd") << "Success!" << std::endl; - ++(d_quantEngine->d_statistics.d_instantiations_guess); - return true; - } - else - { - index--; - } + terms.push_back(rd->getRDomain(f, i)->d_terms[childIndex[i]]); + Trace("inst-alg-rd") + << " " << rd->getRDomain(f, i)->d_terms[childIndex[i]] + << std::endl; } - } while (success); - max_i++; + else + { + Assert(childIndex[i] < term_db_list[ftypes[i]].size()); + terms.push_back(term_db_list[ftypes[i]][childIndex[i]]); + Trace("inst-alg-rd") + << " " << term_db_list[ftypes[i]][childIndex[i]] + << std::endl; + } + } + if (ie->addInstantiation(f, terms)) + { + Trace("inst-alg-rd") << "Success!" << std::endl; + ++(d_quantEngine->d_statistics.d_instantiations_guess); + return true; + } + else + { + index--; + } } - } + } while (success); + max_i++; } } // TODO : term enumerator instantiation? diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index be0f452e4..f011efdfc 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -92,8 +92,12 @@ class InstStrategyEnum : public QuantifiersModule * well-typed term *not* occurring in the current context. * This handles corner cases where there are no well-typed * ground terms in the current context to instantiate with. + * + * The flag isRd indicates whether we are trying relevant domain + * instantiations. If this flag is false, we are trying arbitrary ground + * term instantiations. */ - bool process(Node q, bool fullEffort); + bool process(Node q, bool fullEffort, bool isRd); }; /* class InstStrategyEnum */ } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 96a28cde6..623db032a 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -2,9 +2,9 @@ /*! \file instantiate.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 62e0ddb55..25f333fbb 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -2,9 +2,9 @@ /*! \file instantiate.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/lazy_trie.cpp b/src/theory/quantifiers/lazy_trie.cpp index 35049b8ba..a50352df5 100644 --- a/src/theory/quantifiers/lazy_trie.cpp +++ b/src/theory/quantifiers/lazy_trie.cpp @@ -2,9 +2,9 @@ /*! \file lazy_trie.cpp ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h index 156f1abde..ce6d841cc 100644 --- a/src/theory/quantifiers/lazy_trie.h +++ b/src/theory/quantifiers/lazy_trie.h @@ -2,9 +2,9 @@ /*! \file lazy_trie.h ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp index 752d61489..520088328 100644 --- a/src/theory/quantifiers/local_theory_ext.cpp +++ b/src/theory/quantifiers/local_theory_ext.cpp @@ -2,9 +2,9 @@ /*! \file local_theory_ext.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng + ** Andrew Reynolds, Morgan Deters, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h index b8b0e34fa..7a6182394 100644 --- a/src/theory/quantifiers/local_theory_ext.h +++ b/src/theory/quantifiers/local_theory_ext.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 5b57af14c..203c3d6a7 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2,9 +2,9 @@ /*! \file quant_conflict_find.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters + ** Andrew Reynolds, Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 9fa37a96c..b40840756 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -2,9 +2,9 @@ /*! \file quant_conflict_find.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/quant_epr.cpp b/src/theory/quantifiers/quant_epr.cpp index eedea6767..e03a2c120 100644 --- a/src/theory/quantifiers/quant_epr.cpp +++ b/src/theory/quantifiers/quant_epr.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/quant_epr.h b/src/theory/quantifiers/quant_epr.h index 07569a09b..9eda74d25 100644 --- a/src/theory/quantifiers/quant_epr.h +++ b/src/theory/quantifiers/quant_epr.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/quant_relevance.cpp b/src/theory/quantifiers/quant_relevance.cpp index a05388d17..de54fa05f 100644 --- a/src/theory/quantifiers/quant_relevance.cpp +++ b/src/theory/quantifiers/quant_relevance.cpp @@ -2,9 +2,9 @@ /*! \file quant_relevance.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h index 21017e783..43bb4c548 100644 --- a/src/theory/quantifiers/quant_relevance.h +++ b/src/theory/quantifiers/quant_relevance.h @@ -2,9 +2,9 @@ /*! \file quant_relevance.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index fb5492eb3..808c6006f 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -2,9 +2,9 @@ /*! \file quant_split.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index 6a752fe3f..ec40bc52f 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index b1b34fb98..6d28c574a 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -2,9 +2,9 @@ /*! \file quant_util.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index e324bc36f..3cfd3b2df 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -2,9 +2,9 @@ /*! \file quant_util.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index e3463df0d..d93de6a54 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -2,9 +2,9 @@ /*! \file quantifiers_attributes.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng, Tim King + ** Andrew Reynolds, Paul Meng, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index d3acc9434..46cb5a4ce 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index e2a26f6e6..015bf9c5a 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index a1d6d25c3..e44672d66 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index e62f3513c..bc7538c1f 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -185,9 +185,9 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex) NodeManager* nm = NodeManager::currentNM(); // make the satisfiability query bool needExport = false; - ExprManagerMapCollection varMap; ExprManager em(nm->getOptions()); std::unique_ptr<SmtEngine> queryChecker; + ExprManagerMapCollection varMap; initializeChecker(queryChecker, em, varMap, qy, needExport); Result r = queryChecker->checkSat(); Trace("sygus-qgen-check") << " query: ...got : " << r << std::endl; diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h index f0b3fa565..b283d818b 100644 --- a/src/theory/quantifiers/query_generator.h +++ b/src/theory/quantifiers/query_generator.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 849e73822..071bd7933 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -2,9 +2,9 @@ /*! \file relevant_domain.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -169,7 +169,9 @@ void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool po computeRelevantDomainOpCh( rf, n[i] ); } } - if( n[i].getKind()!=FORALL ){ + // do not recurse under nested closures + if (!n[i].isClosure()) + { bool newHasPol; bool newPol; QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol ); diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 78fe23890..ff419666f 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index ed9666d80..ff42a9c89 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -2,9 +2,9 @@ /*! \file rewrite_engine.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index febcc0126..88a9882ca 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -2,9 +2,9 @@ /*! \file rewrite_engine.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Tim King + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index 851204a84..153ab71cc 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -2,9 +2,9 @@ /*! \file single_inv_partition.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h index 199ab29d4..1a01f3b8b 100644 --- a/src/theory/quantifiers/single_inv_partition.h +++ b/src/theory/quantifiers/single_inv_partition.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 2f12c000c..1d2b869c4 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 5605c8c5f..3db3aa838 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp index 19d39e997..2c6186372 100644 --- a/src/theory/quantifiers/solution_filter.cpp +++ b/src/theory/quantifiers/solution_filter.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h index d162f41f0..80af05eb8 100644 --- a/src/theory/quantifiers/solution_filter.h +++ b/src/theory/quantifiers/solution_filter.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index aa20c1f76..00d040af5 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -2,9 +2,9 @@ /*! \file ce_guided_single_inv.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Andres Noetzli, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index 0de7b4290..93b972fbc 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index 7f7c56f84..074971622 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -2,9 +2,9 @@ /*! \file ce_guided_single_inv_sol.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h index fb0862413..bdafe7bef 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 6aca71ca3..314b43711 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 849a39639..f706e3d97 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -2,9 +2,9 @@ /*! \file cegis.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, Andres Noetzli + ** Andrew Reynolds, Haniel Barbosa, FabianWolff ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 18e313bf0..e34669425 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 972d07af7..4255966c6 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index e8daa4256..b568b8f53 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h index 476a364ea..4d4c85703 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.h +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 9981b5141..bd85ea496 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -476,6 +476,13 @@ bool SygusEnumerator::TermEnumSlave::validateIndex() { Assert(d_index == tc.getNumTerms()); Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : force master...\n"; + // if the size of the master is larger than the size limit, then + // there is no use continuing, since there are no more terms that this + // slave enumerator can return. + if (d_master->getCurrentSize() > d_sizeLim) + { + return false; + } // must push the master index if (!d_master->increment()) { @@ -655,9 +662,14 @@ bool SygusEnumerator::TermEnumMaster::increment() { return false; } + Trace("sygus-enum-summary") << "SygusEnumerator::TermEnumMaster: increment " + << d_tn << "..." << std::endl; d_isIncrementing = true; bool ret = incrementInternal(); d_isIncrementing = false; + Trace("sygus-enum-summary") + << "SygusEnumerator::TermEnumMaster: finished increment " << d_tn + << std::endl; return ret; } @@ -789,7 +801,15 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal() // restart with constructor class one (skip nullary constructors) d_consClassNum = 1; - return incrementInternal(); + + // We break for a round: return the null term when we cross a size + // boundary. This ensures that the necessary breaks are taken, e.g. + // in slave enumerators who may instead want to abandon this call to + // increment master when the size of the master makes their increment + // infeasible. + d_currTermSet = true; + d_currTerm = Node::null(); + return true; } bool incSuccess = false; @@ -819,6 +839,8 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal() // the term was not unique based on rewriting Trace("sygus-enum-debug2") << "master(" << d_tn << "): failed addTerm\n"; + // we will return null (d_currTermSet is true at this point) + Assert(d_currTermSet); d_currTerm = Node::null(); } } diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index 716a047d2..5bfe60f49 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -1,10 +1,10 @@ -/******************** */ +/********************* */ /*! \file sygus_enumerator.h ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index ac7467c00..e44b604d0 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h index 94f37c845..ad1e3331d 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index ddf52001e..f55ce2097 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h index 3f18a65d6..522d6ee8a 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.h +++ b/src/theory/quantifiers/sygus/sygus_explain.h @@ -2,9 +2,9 @@ /*! \file sygus_explain.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, FabianWolff ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 67fa1398e..48da8e8e8 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index bf377bd33..e39943866 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -2,9 +2,9 @@ /*! \file sygus_grammar_cons.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 8e41b6b07..fb6b23132 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index 993d41668..e186fb02c 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -2,9 +2,9 @@ /*! \file sygus_grammar_norm.h ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa, Tim King, Andrew Reynolds + ** Haniel Barbosa, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp index 24aa74c9e..6ad590f28 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp @@ -2,9 +2,9 @@ /*! \file sygus_grammar_red.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h index ce83402c9..eb43b5c3c 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index 5ea01ef57..b494e085e 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index 02c249411..a5b32cb0d 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -2,9 +2,9 @@ /*! \file sygus_invariance.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner + ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp index 3471472fa..42a125ae5 100644 --- a/src/theory/quantifiers/sygus/sygus_module.cpp +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index fef24e9bb..07bce1791 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 7891814be..2ab51f1fb 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -2,9 +2,9 @@ /*! \file sygus_pbe.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, Aina Niemetz + ** Andrew Reynolds, Haniel Barbosa, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index dc7f1cc51..3738c40b7 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index a2454758a..2b9592d4d 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -2,9 +2,9 @@ /*! \file sygus_process_conj.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index 199619699..86e066b6b 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus/sygus_process_conj.h @@ -2,9 +2,9 @@ /*! \file sygus_process_conj.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 09525712f..85a0a4bf8 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -2,9 +2,9 @@ /*! \file sygus_repair_const.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -115,6 +115,7 @@ void SygusRepairConst::initializeChecker(std::unique_ptr<SmtEngine>& checker, try { checker.reset(new SmtEngine(&em)); + checker->setIsInternalSubsolver(); checker->setTimeLimit(options::sygusRepairConstTimeout(), true); checker->setLogic(smt::currentSmtEngine()->getLogicInfo()); // renable options disabled by sygus diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index c6bfd2806..ee23d9732 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -2,9 +2,9 @@ /*! \file sygus_repair_const.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 5d7017a1c..2eb508fde 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -2,9 +2,9 @@ /*! \file sygus_unif.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa + ** Andrew Reynolds, Aina Niemetz, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 0784644f8..f7a218ec0 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index c9db62735..207aa4c8e 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -2,9 +2,9 @@ /*! \file sygus_unif_io.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa + ** Andrew Reynolds, Haniel Barbosa, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -161,7 +161,12 @@ bool UnifContextIo::getStringIncrement(SygusUnifIo* sui, if (d_vals[j] == sui->d_true) { // example is active in this context - Assert(vals[j].isConst()); + if (!vals[j].isConst()) + { + // the value is unknown, thus we cannot use it to increment the strings + // position + return false; + } String mystr = vals[j].getConst<String>(); ival = mystr.size(); if (mystr.size() <= ex_vals[j].size()) @@ -199,7 +204,11 @@ bool UnifContextIo::isStringSolved(SygusUnifIo* sui, if (d_vals[j] == sui->d_true) { // example is active in this context - Assert(vals[j].isConst()); + if (!vals[j].isConst()) + { + // value is unknown, thus it does not solve + return false; + } String mystr = vals[j].getConst<String>(); if (ex_vals[j] != mystr) { @@ -448,12 +457,23 @@ void SubsumeTrie::getLeavesInternal(const std::vector<Node>& vals, ++it) { int new_status = status; - // if the current value is true + bool success = true; + // If the current value is true, then this is a relevant point. + // We must consider the value of this child. if (curr_val_true) { - if (status != 0) + if (it->first.isNull()) { - Assert(it->first.isConst() && it->first.getType().isBoolean()); + // The value of this child is unknown on this point, hence we + // do not recurse + success = false; + } + else if (status != 0) + { + // if the status is not zero (indicating that we have a mix of T/F), + // then we must compute the new status. + Assert(it->first.getType().isBoolean()); + Assert(it->first.isConst()); new_status = (it->first.getConst<bool>() ? 1 : -1); if (status != -2 && new_status != status) { @@ -461,7 +481,10 @@ void SubsumeTrie::getLeavesInternal(const std::vector<Node>& vals, } } } - it->second.getLeavesInternal(vals, pol, v, index + 1, new_status); + if (success) + { + it->second.getLeavesInternal(vals, pol, v, index + 1, new_status); + } } } } @@ -641,23 +664,41 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) for (unsigned j = 0, size = itsr->second.size(); j < size; j++) { Node res = itsr->second[j]; - Assert(res.isConst()); + // The value of this term for this example, or the truth value of + // the I/O pair if the role of this enumerator is enum_io. Node resb; if (eiv.getRole() == enum_io) { Node out = d_examples_out[j]; Assert(out.isConst()); - resb = res == out ? d_true : d_false; + // If the result is not constant, then we assume that it does + // not satisfy the example. This is a safe underapproximation + // of the good behavior of the current term, that is, we only + // produce solutions whose values are fully evaluatable on all input + // points. Notice that terms may be used as leaves of decision + // trees that are fully evaluatable on points in that branch, but + // are not evaluatable on others, e.g. (head x) in the solution: + // (ite ((_ is cons) x) (head x) 5) + resb = (res.isConst() && res == out) ? d_true : d_false; } else { - resb = res; + // We only set resb if it is constant, otherwise it remains null. + // This indicates its value cannot be determined. + if (res.isConst()) + { + resb = res; + } } cond_vals[resb] = true; results.push_back(resb); if (Trace.isOn("sygus-sui-enum")) { - if (resb.getType().isBoolean()) + if (resb.isNull()) + { + Trace("sygus-sui-enum") << "_"; + } + else if (resb.getType().isBoolean()) { Trace("sygus-sui-enum") << (resb == d_true ? "1" : "0"); } @@ -677,6 +718,7 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) std::vector<Node> subsume; if (cond_vals.find(d_false) == cond_vals.end()) { + Assert(cond_vals.size() == 1); // it is the entire solution, we are done Trace("sygus-sui-enum") << " ...success, full solution added to PBE pool : " @@ -917,23 +959,27 @@ bool SygusUnifIo::getExplanationForEnumeratorExclude( std::vector<unsigned> cmp_indices; for (unsigned i = 0, size = results.size(); i < size; i++) { - Assert(results[i].isConst()); - Assert(d_examples_out[i].isConst()); - Trace("sygus-sui-cterm-debug") - << " " << results[i] << " <> " << d_examples_out[i]; - Node cont = nm->mkNode(STRING_STRCTN, d_examples_out[i], results[i]); - Node contr = Rewriter::rewrite(cont); - if (contr == d_false) - { - cmp_indices.push_back(i); - Trace("sygus-sui-cterm-debug") << "...not contained." << std::endl; - } - else + // If the result is not constant, then it is worthless. It does not + // impact whether the term is excluded. + if (results[i].isConst()) { - Trace("sygus-sui-cterm-debug") << "...contained." << std::endl; - if (isConditional) + Assert(d_examples_out[i].isConst()); + Trace("sygus-sui-cterm-debug") + << " " << results[i] << " <> " << d_examples_out[i]; + Node cont = nm->mkNode(STRING_STRCTN, d_examples_out[i], results[i]); + Node contr = Rewriter::rewrite(cont); + if (contr == d_false) { - return false; + cmp_indices.push_back(i); + Trace("sygus-sui-cterm-debug") << "...not contained." << std::endl; + } + else + { + Trace("sygus-sui-cterm-debug") << "...contained." << std::endl; + if (isConditional) + { + return false; + } } } } diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 7f48645bf..fced29871 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -218,7 +218,24 @@ class SubsumeTrie int status, bool checkExistsOnly, bool checkSubsume); - /** helper function for above functions */ + /** helper function for above functions + * + * This adds to v[-1], v[0], v[1] the children of the trie that occur + * along paths that contain only false (v[-1]), a mix of true/false (v[0]), + * and only true (v[1]) values for respectively for relevant points. + * + * vals/pol is used to determine the relevant points, which impacts which + * paths of the trie to traverse on this call. + * In particular, all points such that (pol ? vals[index] : !vals[index]) + * are relevant. + * + * Paths that contain an unknown value for any relevant point are not + * traversed. In the larger picture, this ensures that terms are not used in a + * way such that their unknown value is relevant to the overall behavior of + * a synthesis solution. + * + * status holds the current value of v (0,1,-1) that we will be adding to. + */ void getLeavesInternal(const std::vector<Node>& vals, bool pol, std::map<int, std::vector<Node>>& v, diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index ee07efdfe..3514ccbeb 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index 179a5ac16..0f0b2c533 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 3cbac1eaa..acf5a2d7f 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index 41923f7a1..54933a2af 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index e25e8a225..756e1f791 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -2,9 +2,9 @@ /*! \file synth_conjecture.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Haniel Barbosa + ** Andrew Reynolds, Haniel Barbosa, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -540,6 +540,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) Trace("cegqi-engine") << "Check side condition..." << std::endl; Trace("cegqi-debug") << "Check side condition : " << sc << std::endl; SmtEngine scSmt(nm->toExprManager()); + scSmt.setIsInternalSubsolver(); scSmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); scSmt.assertFormula(sc.toExpr()); Result r = scSmt.checkSat(); @@ -572,6 +573,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) { Trace("cegqi-engine") << " *** Verify with subcall..." << std::endl; SmtEngine verifySmt(nm->toExprManager()); + verifySmt.setIsInternalSubsolver(); verifySmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); verifySmt.assertFormula(query.toExpr()); Result r = verifySmt.checkSat(); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index cf6178fdb..923d1d57c 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -2,9 +2,9 @@ /*! \file synth_conjecture.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Haniel Barbosa + ** Andrew Reynolds, Haniel Barbosa, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index d3eff1750..fc1ed938d 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -159,6 +159,7 @@ void SynthEngine::assignConjecture(Node q) { // create new smt engine to do quantifier elimination SmtEngine smt_qe(nm->toExprManager()); + smt_qe.setIsInternalSubsolver(); smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo()); Trace("cegqi-qep") << "Property is non-ground single invocation, run " "QE to obtain single invocation." diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index a7346b888..2dbd20827 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -2,9 +2,9 @@ /*! \file synth_engine.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Tim King + ** Andrew Reynolds, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 9198f7e56..b1e6dc96d 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -2,9 +2,9 @@ /*! \file term_database_sygus.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, Aina Niemetz + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 7a522ded6..cdeaf1803 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -2,9 +2,9 @@ /*! \file term_database_sygus.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index f1908fc19..10d7ef6ab 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -2,9 +2,9 @@ /*! \file sygus_sampler.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -40,7 +40,6 @@ void SygusSampler::initialize(TypeNode tn, d_tds = nullptr; d_use_sygus_type = false; d_is_valid = true; - d_tn = tn; d_ftn = TypeNode::null(); d_type_vars.clear(); d_vars.clear(); @@ -95,7 +94,6 @@ void SygusSampler::initializeSygus(TermDbSygus* tds, Assert(d_ftn.isDatatype()); const Datatype& dt = static_cast<DatatypeType>(d_ftn.toType()).getDatatype(); Assert(dt.isSygus()); - d_tn = TypeNode::fromType(dt.getSygusType()); Trace("sygus-sample") << "Register sampler for " << f << std::endl; @@ -264,28 +262,30 @@ bool SygusSampler::PtTrie::add(std::vector<Node>& pt) Node SygusSampler::registerTerm(Node n, bool forceKeep) { - if (d_is_valid) + if (!d_is_valid) { - Node bn = n; - // if this is a sygus type, get its builtin analog - if (d_use_sygus_type) - { - Assert(!d_ftn.isNull()); - bn = d_tds->sygusToBuiltin(n); - Assert(d_builtin_to_sygus.find(bn) == d_builtin_to_sygus.end() - || d_builtin_to_sygus[bn] == n); - d_builtin_to_sygus[bn] = n; - } - Assert(bn.getType() == d_tn); - Node res = d_trie.add(bn, this, 0, d_samples.size(), forceKeep); - if (d_use_sygus_type) - { - Assert(d_builtin_to_sygus.find(res) != d_builtin_to_sygus.end()); - res = res != bn ? d_builtin_to_sygus[res] : n; - } - return res; + // do nothing + return n; + } + Node bn = n; + TypeNode tn = n.getType(); + // If we are using sygus types, get the builtin analog of n. + if (d_use_sygus_type) + { + bn = d_tds->sygusToBuiltin(n); + d_builtin_to_sygus[tn][bn] = n; + } + // cache based on the (original) type of n + Node res = d_trie[tn].add(bn, this, 0, d_samples.size(), forceKeep); + // If we are using sygus types, map back to an original. + // Notice that d_builtin_to_sygus is not necessarily bijective. + if (d_use_sygus_type) + { + std::map<Node, Node>& bts = d_builtin_to_sygus[tn]; + Assert(bts.find(res) != bts.end()); + res = res != bn ? bts[res] : n; } - return n; + return res; } bool SygusSampler::isContiguous(Node n) diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 28f715b34..3a2c42b9d 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -2,9 +2,9 @@ /*! \file sygus_sampler.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner + ** Andrew Reynolds, FabianWolff, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -194,14 +194,15 @@ class SygusSampler : public LazyTrieEvaluator }; /** a trie for samples */ PtTrie d_samples_trie; - /** type of nodes we will be registering with this class */ - TypeNode d_tn; /** the sygus type for this sampler (if applicable). */ TypeNode d_ftn; - /** whether we are registering terms of type d_ftn */ + /** whether we are registering terms of sygus types with this sampler */ bool d_use_sygus_type; - /** map from builtin terms to the sygus term they correspond to */ - std::map<Node, Node> d_builtin_to_sygus; + /** + * For each (sygus) type, a map from builtin terms to the sygus term they + * correspond to. + */ + std::map<TypeNode, std::map<Node, Node> > d_builtin_to_sygus; /** all variables we are sampling values for */ std::vector<Node> d_vars; /** type variables @@ -235,8 +236,22 @@ class SygusSampler : public LazyTrieEvaluator * that type. */ std::map<TypeNode, std::vector<Node> > d_type_consts; - /** the lazy trie */ - LazyTrie d_trie; + /** a lazy trie for each type + * + * This stores the evaluation of all terms registered to this class. + * + * Notice if we are registering sygus terms with this class, then terms + * are grouped into this trie according to their sygus type, and not their + * builtin type. For example, for grammar: + * A -> x | B+1 + * B -> x | 0 | 1 | B+B + * If we register C^B_+( C^B_x(), C^B_0() ) and C^A_x() with this class, + * then x+0 is registered to d_trie[B] and x is registered to d_trie[A], + * and no rewrite rule is reported. The reason for this is that otherwise + * we would end up reporting many useless rewrites since the same builtin + * term can be generated by multiple sygus types (e.g. C^B_x() and C^A_x()). + */ + std::map<TypeNode, LazyTrie> d_trie; /** is this sampler valid? * * A sampler can be invalid if sample points cannot be generated for a type diff --git a/src/theory/quantifiers/term_canonize.cpp b/src/theory/quantifiers/term_canonize.cpp index d257198d9..9817da5a1 100644 --- a/src/theory/quantifiers/term_canonize.cpp +++ b/src/theory/quantifiers/term_canonize.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/term_canonize.h b/src/theory/quantifiers/term_canonize.h index e23627271..b433992c8 100644 --- a/src/theory/quantifiers/term_canonize.h +++ b/src/theory/quantifiers/term_canonize.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 44c5586c3..472e2561f 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -2,9 +2,9 @@ /*! \file term_database.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Francois Bobot + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index cc9a24d08..3cc8dbaa9 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/term_enumeration.cpp b/src/theory/quantifiers/term_enumeration.cpp index 8e3219768..0336700ad 100644 --- a/src/theory/quantifiers/term_enumeration.cpp +++ b/src/theory/quantifiers/term_enumeration.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -87,6 +87,26 @@ bool TermEnumeration::mayComplete(TypeNode tn, unsigned maxCard) return mc; } +bool TermEnumeration::getDomain(TypeNode tn, std::vector<Node>& dom) +{ + if (!mayComplete(tn)) + { + return false; + } + Node curre; + unsigned counter = 0; + do + { + curre = getEnumerateTerm(tn, counter); + counter++; + if (!curre.isNull()) + { + dom.push_back(curre); + } + } while (!curre.isNull()); + return true; +} + } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h index cf25335f4..ed6529ef1 100644 --- a/src/theory/quantifiers/term_enumeration.h +++ b/src/theory/quantifiers/term_enumeration.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -56,6 +56,14 @@ class TermEnumeration */ static bool mayComplete(TypeNode tn, unsigned cardMax); + /** get domain + * + * If tn is a type such that mayComplete(tn) returns true, this method + * adds all domain elements of tn to dom and returns true. Otherwise, this + * method returns false. + */ + bool getDomain(TypeNode tn, std::vector<Node>& dom); + private: /** ground terms enumerated for types */ std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction> diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 4c9cf2c8d..065096607 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -2,9 +2,9 @@ /*! \file term_util.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng, Yoni Zohar + ** Andrew Reynolds, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 820821991..061da81df 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -2,9 +2,9 @@ /*! \file term_util.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 6f647aeb1..f24a4bb2b 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -2,9 +2,9 @@ /*! \file theory_quantifiers.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -38,8 +38,6 @@ using namespace CVC4::theory::quantifiers; TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo) { - d_numInstantiations = 0; - d_baseDecLevel = -1; out.handleUserAttribute( "axiom", this ); out.handleUserAttribute( "conjecture", this ); out.handleUserAttribute( "fun-def", this ); @@ -71,13 +69,6 @@ void TheoryQuantifiers::preRegisterTerm(TNode n) { return; } Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl; - if (options::cbqi() && !options::recurseCbqi() - && TermUtil::hasInstConstAttr(n)) - { - Debug("quantifiers-prereg") - << "TheoryQuantifiers::preRegisterTerm() done, unused " << n << endl; - return; - } // Preregister the quantified formula. // This initializes the modules used for handling n in this user context. getQuantifiersEngine()->preRegisterQuantifier(n); @@ -135,7 +126,7 @@ void TheoryQuantifiers::check(Effort e) { Trace("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl; switch(assertion.getKind()) { case kind::FORALL: - assertUniversal( assertion ); + getQuantifiersEngine()->assertQuantifier(assertion, true); break; case kind::INST_CLOSURE: getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true ); @@ -150,7 +141,7 @@ void TheoryQuantifiers::check(Effort e) { { switch( assertion[0].getKind()) { case kind::FORALL: - assertExistential( assertion ); + getQuantifiersEngine()->assertQuantifier(assertion[0], false); break; case kind::EQUAL: //do nothing @@ -171,20 +162,6 @@ void TheoryQuantifiers::check(Effort e) { getQuantifiersEngine()->check( e ); } -void TheoryQuantifiers::assertUniversal( Node n ){ - Assert( n.getKind()==FORALL ); - if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){ - getQuantifiersEngine()->assertQuantifier( n, true ); - } -} - -void TheoryQuantifiers::assertExistential( Node n ){ - Assert( n.getKind()== NOT && n[0].getKind()==FORALL ); - if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n[0]) ){ - getQuantifiersEngine()->assertQuantifier( n[0], false ); - } -} - void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){ QuantAttributes::setUserAttribute( attr, n, node_values, str_value ); } diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 55047fe2b..f6e19f700 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -2,9 +2,9 @@ /*! \file theory_quantifiers.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andrew Reynolds + ** Tim King, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -56,13 +56,6 @@ class TheoryQuantifiers : public Theory { std::vector<Node> node_values, std::string str_value) override; - private: - void assertUniversal( Node n ); - void assertExistential( Node n ); - /** number of instantiations */ - int d_numInstantiations; - int d_baseDecLevel; - };/* class TheoryQuantifiers */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index bac3ca58f..18aa7f6ee 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim |