Error while trying to use the synthesis feature

[sderrien]

Hello,

I am trying to use Uclid5 to perform some automatic control synthesis in the context of a High-Level Synthesis (HLS) flow, using the built-in synthesis feature. While I’ve been able to get a few simple examples to work, I often encounter the following error, which I don’t understand.

Could anyone help me figure out what I’m doing wrong (an example that reproduces the error is provided below)?

Exception in thread "main" uclid.Utils$RuntimeError: SExpr model parser error: '[keyword])' expected but ErrorToken('"' expected but found) found.
In: (error "Parse Error: :16.37: Symbol '->' not declared as a type")
at uclid.smt.SExprParser$.parseModel(SExprParser.scala:700)
at uclid.smt.SMTLIB2Model.(SMTLIB2Interface.scala:398)
at uclid.smt.SYNTLIBModel.(SynthLibInterface.scala:48)

Thank you in advance for your help !

Regards,

Steven Derrien

=====================================================================
module main {

const INITX : integer;


function slow(a : integer) : integer;
function fast(a : integer) : integer;
function cond(a : integer) : boolean;

define golden_comp(a : integer) : integer = if (cond(a)) then slow(a) else fast(a);

var t, x : integer;
var s_x,s_x1,s_x2 : integer;
var slow_x0, slow_x1, slow_x2, slow_x3, slow_x4 : integer;
var golden: integer;

// FSM
var cs : bv3;

synthesis function loop() : bv3 ;

define nxt(cs : bv3, cond : boolean) : bv3 =
	if (cs==0bv3) then
	  	if(cond) then 
	  		1bv3 
	  	else 
	  		0bv3
	else 
		if (cs>loop()) then 
			0bv3 
		else 
			cs + 1bv3;
		  

// ---------- Initialisation ----------
init {
	t = 0 ;
	x = 0;
	s_x = INITX; 
	cs=0bv3;
}

next {

  s_x ' = if (cs==0bv3) then fast(s_x) else slow_x3;

  slow_x3' = slow_x2; 
  slow_x2' = slow_x1; 
  slow_x1' = slow_x0; 
  slow_x0' = slow(s_x); 

  golden'= golden_comp(golden); 

  cs'  = nxt(cs, cond(s_x)) ;
  t '= t+1;
  
}

// ---------- Invariants ----------
const N : integer=5;


invariant forward_sim : (t> N) ==> 
	(
	(history(s_x,5)==history(golden,5) && (((history(cs,5))==0bv3)) ) ==> 
		(  
	  		((history(golden,4) ==  history(s_x,4)) && (((history(cs,4))==0bv3 ))) 
	  		|| 
	  		((history(golden,4) ==            s_x)) && ((cs)            ==0bv3 && (history(cs,1))!=0bv3    && (history(cs,2))!=0bv3    && (history(cs,3))!=0bv3    && (history(cs,4))!=0bv3   ))
	   
	  );

control {
	vobj= induction(N);
	check;
	print_results;
	vobj.print_cex(s_x,golden,cs,cond(s_x),fast(s_x),slow(s_x),slow_x1);
}

}

[polgreen]

Hi,

Unfortunately, I don't think you're going to get the underlying solver to work on this query, because it involves universally quantifying over uninterpreted functions.

Since, officially, SyGuS doesn't support uninterpreted functions, we have represented the UFs which would normally be (declare-fun const_slow (Int) Int ) as higher order variables, e.g., (declare-var const_slow (-> Int Int )).

The error message you are seeing is because we didn't add HO for higher order to the logic at the top of the file. The logic should be HO_ALL, not ALL.

I've attached the SyGuS file as it should be, so you can run cvc5 on it directly, but i don't think you'll have much joy. I've tried it for 10 minutes on my laptop and the synthesis got stuck verifying one candidate

debug.sl.zip

(You can produce the SyGuS file yourself with the command line arguments uclid myfile -y "cvc5" -g "filename").

I'll need to think about whether we want to generate higher-order logic SyGuS files with the correct logic, or throw an error if the user asks for synthesis when the model contains uninterpreted functions

[sderrien]

Thanks a lot for the feedback.

I am very new to SyGus, and I was actually using uninterpreted function in the hope of simplifying the problem state space by abstracting the computation pipeline, seems it was not a good idea. I'll try a different path.

[polgreen]

Yes, using UFs makes the problem harder, because the synthesis task is "find a synthesis function that makes the verification pass for all possible assignments to free variables and functions".

So, if you have a UF, you have to find a synthesis function that makes the verification pass for all possible interpretations of that UF.