-
Notifications
You must be signed in to change notification settings - Fork 4
Open
Description
Hello,
I'm trying to use your library like in the script below to process a SyGuS specification containing Real sort:
from sys import path as pylib #im naming it as pylib so that we won't get confused between os.path and sys.path
import os
pylib += [os.path.abspath(r'../../submodules/sygus_tools/sygus')]
from src.v2.parser import SygusV2Parser
from src.v2.printer import SygusV2ASTPrinter
from src.symbol_table_builder import SymbolTableBuilder
text1 = """
(set-logic NRA)
(synth-fun gravity ((m1 Real)(m2 Real)(r Real)) Real)
(declare-var m1 Real)
(declare-var m2 Real)
(declare-var r Real)
(constraint (= (gravity 16.07231 1.04184 1.55562) 0.0000000004618048547558316))
(constraint (= (gravity 3.6475 6.42314 9.8414) 0.000000000016144147736033107))
(constraint (= (gravity 12.19278 5.76768 12.4051) 0.00000000003049927795683856))
(constraint (=> (and (> m1 0.0) (> m2 0.0) (> r 0.0)) (= (gravity m1 m2 r) (gravity m2 m1 r))))
(constraint (=> (and (> m1 0.0) (> m2 0.0) (> r 0.0)) (>= (gravity m1 m2 r) 0.0)))
(constraint (forall ((m1 Real)(m2 Real)(r Real)(cdgp.P2.m1 Real)) (=> (and (> cdgp.P2.m1 0.0) (> m1 0.0) (> m2 0.0) (> r 0.0)) (=> (> cdgp.P2.m1 m1) (> (gravity cdgp.P2.m1 m2 r) (gravity m1 m2 r))))))
(constraint (forall ((m1 Real)(m2 Real)(r Real)(cdgp.P3.m2 Real)) (=> (and (> cdgp.P3.m2 0.0) (> m1 0.0) (> m2 0.0) (> r 0.0)) (=> (> cdgp.P3.m2 m2) (> (gravity m1 cdgp.P3.m2 r) (gravity m1 m2 r))))))
(check-synth)
"""
parser = SygusV2Parser()
program = parser.parse(text1)
symbol_table = SymbolTableBuilder.run(program)
print(SygusV2ASTPrinter.run(program, symbol_table))
but I get the following error:
Syntax error at token: TK_REAL, Real
At: 3:25 -- 3:25
Could this be because NRA is not recognized as a SyGuS logic and does not add Real to stack of allowable sorts? But after changing the logic to SLIA or LIA, and sorts to Int, I get error Syntax error at token: TK_INT, Int.
Metadata
Metadata
Assignees
Labels
No labels