From f3590092818d9eab9d961ea602093029ff472a85 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 10 Jul 2017 14:06:52 -0500 Subject: Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions. --- src/options/Makefile.am | 1 + 1 file changed, 1 insertion(+) (limited to 'src/options/Makefile.am') diff --git a/src/options/Makefile.am b/src/options/Makefile.am index 5a9fa54e6..ff889bcb2 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -229,6 +229,7 @@ liboptions_la_SOURCES = \ base_handlers.h \ bv_bitblast_mode.cpp \ bv_bitblast_mode.h \ + datatypes_modes.h \ decision_mode.cpp \ decision_mode.h \ decision_weight.h \ -- cgit v1.2.3