SyGuS term size limit (#1262)

* Add option sygus-abort-size, which tells the enumerative SyGuS solver to abort when it reaches a given term size.

* Apply clang format.

diff --git a/src/options/datatypes_options b/src/options/datatypes_options
index d4d3e941c2dfd2cf826a6884abb4ac8122e630b5..5163cf35d77c232cf3cb1abe9617eb680b1887eb 100644 (file)
--- a/src/options/datatypes_options
+++ b/src/options/datatypes_options
@@ -47,5 +47,7 @@ option sygusFair --sygus-fair=MODE CVC4::theory::SygusFairMode :default CVC4::th
   if and how to apply fairness for sygus
 option sygusFairMax --sygus-fair-max bool :default true
   use max instead of sum for multi-function sygus conjectures
+option sygusAbortSize --sygus-abort-size=N int :default -1
+  tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)
   
 endmodule

diff --git a/src/options/uf_options b/src/options/uf_options
index 7e1cbdb1700bd12b594426d12fde7f871881e77f..c93ccf864cc98e9aca421db28b245bbcb5d5c5b5 100644 (file)
--- a/src/options/uf_options
+++ b/src/options/uf_options
@@ -22,7 +22,7 @@ option ufssTotalityLimited --uf-ss-totality-limited=N int :default -1
 option ufssTotalitySymBreak --uf-ss-totality-sym-break bool :default false
  apply symmetry breaking for totality axioms
 option ufssAbortCardinality --uf-ss-abort-card=N int :default -1
- tells the uf strong solver a cardinality to abort at (-1 == no limit, default)
+ tells the uf strong solver to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)
 option ufssExplainedCliques --uf-ss-explained-cliques bool :default false
  use explained clique lemmas for uf strong solver
 option ufssSimpleCliques --uf-ss-simple-cliques bool :default true

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 5d48c1ce2d9745962db1bcb7721ae72a292cf542..4999114eb33bb1f51552265520e5c0e53be57520 100644 (file)
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -1347,6 +1347,12 @@ Node SygusSymBreakNew::SearchSizeInfo::getFairnessLiteral( unsigned s, TheoryDat
   if( options::sygusFair()!=SYGUS_FAIR_NONE ){
     std::map< unsigned, Node >::iterator it = d_lits.find( s );
     if( it==d_lits.end() ){
+      if (options::sygusAbortSize() != -1 &&
+          static_cast<int>(s) > options::sygusAbortSize()) {
+        Message() << "Maximum term size (" << options::sygusAbortSize()
+                  << ") for enumerative SyGuS exceeded." << std::endl;
+        exit(1);
+      }
       Assert( !d_this.isNull() );
       Node c = NodeManager::currentNM()->mkConst( Rational( s ) );
       Node lit = NodeManager::currentNM()->mkNode( DT_SYGUS_BOUND, d_this, c );

diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index e7efba325920ff56c3a85667660b06c216e45372..4b6a326cf29f52dd58118c1850db66cbf7e1a5cb 100644 (file)
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1157,8 +1157,10 @@ void SortModel::allocateCardinality( OutputChannel* out ){
   }while( increment );
 
   //check for abort case
-  if( options::ufssAbortCardinality()==d_aloc_cardinality ){
-    Message() << "Maximum cardinality reached." << std::endl;
+  if (options::ufssAbortCardinality() != -1 &&
+      d_aloc_cardinality >= options::ufssAbortCardinality()) {
+    Message() << "Maximum cardinality (" << options::ufssAbortCardinality()
+              << ")  for finite model finding exceeded." << std::endl;
     exit( 1 );
   }else{
     if( applyTotality( d_aloc_cardinality ) ){